documentation cleanup

- use a style that only shows the "Proof." command on mouseover
- limit the depth of the ToC to 2
- clean up headers to yield a cleaner ToC

Author: chdoc

Makefile.coq.local

@@ -12,7 +12,7 @@ DOCDIR = docs
 COQDOCDIR = $(DOCDIR)/coqdoc
 
 COQDOCHTMLFLAGS = --toc -s --external 'http://math-comp.github.io/htmldoc/' mathcomp --html \
-  --with-header $(HEADER) --with-footer $(FOOTER) --index indexpage --parse-comments
+  --with-header $(HEADER) --with-footer $(FOOTER) --index indexpage --parse-comments --toc-depth 2
 
 coqdoc: $(GLOBFILES) $(VFILES) $(HEADER) $(FOOTER) $(RESOURCES)
 	$(SHOW)'COQDOC -d $(COQDOCDIR)'

coqdocjs

@@ -17,7 +17,7 @@ Qed.
 Lemma leq_subl n m o : n <= m -> n - o <= m.
 Proof. move => A. rewrite -[m]subn0. exact: leq_sub. Qed.
 
-(** ** Lemmas on [index], [mask], and [subseq] *)
+(** *** Lemmas on [index] and [subseq] *)
 (** could go to seq.v *)
 
 Lemma mem2_index (T : eqType) (x y : T) (s : seq T) : 
@@ -41,9 +41,6 @@ rewrite -!mem2_index ?mem2E // => [?|]; last exact: (mem_subseq sub_s1_s2).
 exact: subseq_trans sub_s1_s2.
 Qed.
 
-(** ** Lemmas on [next] and [rot] *)
-(** could go to path.v *)
-
 Section Path.
 
 Lemma eq_traject (T : Type) (f g : T -> T) : f =1 g -> traject f =2 traject g.
@@ -115,7 +112,7 @@ move=> inj_f; case: s => //= a s.
 by elim: s a {2 4}a => /= [|y s IHs] a b; rewrite inj_eq // ?IHs -fun_if.
 Qed.
 
-(** ** Lemmas on [index] *)
+(** *** Lemmas on [index] *)
 (** could go to [fingraph.v] *)
 
 Lemma eq_findex (T : finType) (f g : T -> T) : 

theories/arc.v

@@ -8,7 +8,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Set Bullet Behavior "Strict Subproofs". 
 
-(** * Completeness *)
+(** * Completeness of the 2pdom axioms *)
 
 Section s.
 Variable A: Type. 
@@ -153,10 +153,8 @@ Proof.
   apply relabel2_iso=>//.
   case=>//=??/=->//.  
 Qed.
-
-(** ** Main Result *)
 
-(* main completeness theorem *)
+(** main completeness theorem *)
 Theorem completeness (u v: term): graph_of_term u ≃2p graph_of_term v -> u ≡ v.
 Proof.
   move=>/tgraph_graph_iso h.
@@ -168,7 +166,7 @@ Proof.
   apply normal_iso. by rewrite HF'. 
 Qed.
 
-(* actually an iff since graphs from a 2pdom algebra *)
+(** actually an iff since graphs from a 2pdom algebra *)
 Theorem soundness_and_completeness (u v: term): graph_of_term u ≃2p graph_of_term v <-> u ≡ v.
 Proof.
   split => [|uv]; first exact: completeness.

theories/completeness.v

@@ -1189,7 +1189,7 @@ Proof.
 Qed.
 
 
-(** * k-connectivity *)
+(** ** k-connectivity *)
 
 Definition kconnected (k : nat) (G : sgraph) := 
   k < #|G| /\ forall S : {set G}, vseparator S -> k <= #|S|.

theories/connectivity.v

@@ -7,9 +7,8 @@ Unset Printing Implicit Defensive.
 
 Set Bullet Behavior "Strict Subproofs".
 
-(**********************************************************************************)
-(** * Domination Theory                                                           *)
-(**********************************************************************************)
+(** * Domination Theory *)
+
 (** ** Hereditary and superhereditary properties *)
 Section Hereditary.
 Variable (T : finType).

theories/dom.v

@@ -17,7 +17,7 @@ Lemma plain_face (D : hypermap) (x : D) :
   plain D -> face x = finv node (edge x).
 Proof. by move=> plainD; rewrite -plain_eq' // finv_f. Qed.
 
-(** * Hypermaps as embeddings of (planar) grahs *)
+(** * Hypermaps as Embeddings of (planar) Grahps *)
 
 (** This is mainly usedful when takling about embeddings, as hypermaps
 cannot represent isolated vertices. *)

theories/embedding.v

@@ -25,9 +25,11 @@ Local Notation link_rel := checkpoint.link_rel.
    (the latter start from a 2pdom term rather than a 2p term) *)
 Definition graph_of_term: term sym -> graph2 := eval (fun a : flat sym => @g2_var _ _ a).
 
-(** * Term Extraction Function *)
+(** * Term Extraction for 2p-graphs in TW2 *)
 
-(** ** Termination Metric *)
+(** ** Extraction function for connected graphs *)
+
+(** *** Termination Metric *)
 
 Definition term_of_measure (G : graph2) :=
   (input == output :> G) + 2*#|edge G|.
@@ -79,7 +81,7 @@ Proof.
   move: He. by rewrite !inE => /orP[/andP[/eqP<- _]|/andP[_ /eqP<-]].
 Qed.
 
-(** ** Subroutines *)
+(** *** Subroutines *)
 
 Definition lens (G : graph2) := 
   [&& edge_set G (@bag G IO input)  == set0 ,
@@ -216,7 +218,7 @@ Definition tm_ (G : graph2) (e : edge G): term sym :=
 
 Definition tmEs (G : graph2) : seq (term sym) := [seq tm_ e | e in edge_set G IO].
 
-(** ** The Extraction Functional *)
+(** *** The Extraction Functional *)
 
 (** Here we define the extraction function. The case distinctions are chosen
 such that we can make use of induced subgraphs (rather than the more generic
@@ -256,7 +258,7 @@ Definition term_of_rec (term_of : graph2 -> term sym) (G : graph2) :=
 
 Definition term_of := Fix top term_of_measure term_of_rec.
 
-(** ** Termination Argument *)
+(** *** Termination Argument *)
 
 
 Notation sigraph := cp_minor.igraph.

theories/extraction_def.v

@@ -21,7 +21,7 @@ Notation graph2 := (graph2 unit (flat sym)).
 Notation g2_top := (g2_top : graph2).
 Notation g2_one := (g2_one : graph2).
 
-(** * Isomorphim Theorem *)
+(** ** Correctness of the Extraction Function *)
 
 (** In this file we prove correctness of the extraction function. This
 mainly amounts to establishing a variety of isomorphisms corresponding

theories/extraction_iso.v

@@ -21,7 +21,7 @@ Notation graph2 := (graph2 unit (flat sym)).
 Open Scope ptt_ops.
 
 
-(** * Extraction from Disconnected Graphs *)
+(** ** Extraction from Disconnected Graphs *)
 
 Arguments iso_id {Lv Le G}.
 Arguments merge_union_K_l [Lv Le F K i o h] k.