From 2a1978c0c7e3b3bee8c1d912232c9e3bb89a5746 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Fri, 28 Oct 2022 23:34:11 +0200
Subject: [PATCH 1/6] move vernacular files to theories directory

---
 _CoqProject                             | 33 +++++++++++++------------
 AVL.v => theories/AVL.v                 |  0
 AVLproofs.v => theories/AVLproofs.v     |  0
 Comparisons.v => theories/Comparisons.v |  0
 Facts.v => theories/Facts.v             |  0
 GenTree.v => theories/GenTree.v         |  0
 Interface.v => theories/Interface.v     |  0
 MMaps.v => theories/MMaps.v             |  0
 OrdList.v => theories/OrdList.v         |  0
 Positive.v => theories/Positive.v       |  0
 RBT.v => theories/RBT.v                 |  0
 RBTproofs.v => theories/RBTproofs.v     |  0
 Raw.v => theories/Raw.v                 |  0
 Utils.v => theories/Utils.v             |  0
 WeakList.v => theories/WeakList.v       |  0
 demo.v => theories/demo.v               |  0
 16 files changed, 17 insertions(+), 16 deletions(-)
 rename AVL.v => theories/AVL.v (100%)
 rename AVLproofs.v => theories/AVLproofs.v (100%)
 rename Comparisons.v => theories/Comparisons.v (100%)
 rename Facts.v => theories/Facts.v (100%)
 rename GenTree.v => theories/GenTree.v (100%)
 rename Interface.v => theories/Interface.v (100%)
 rename MMaps.v => theories/MMaps.v (100%)
 rename OrdList.v => theories/OrdList.v (100%)
 rename Positive.v => theories/Positive.v (100%)
 rename RBT.v => theories/RBT.v (100%)
 rename RBTproofs.v => theories/RBTproofs.v (100%)
 rename Raw.v => theories/Raw.v (100%)
 rename Utils.v => theories/Utils.v (100%)
 rename WeakList.v => theories/WeakList.v (100%)
 rename demo.v => theories/demo.v (100%)

diff --git a/_CoqProject b/_CoqProject
index fcc265e..2629184 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,16 +1,17 @@
--R . MMaps
-Utils.v
-Comparisons.v
-Interface.v
-Facts.v
-Raw.v
-WeakList.v
-OrdList.v
-Positive.v
-GenTree.v
-AVL.v
-AVLproofs.v
-RBT.v
-RBTproofs.v
-MMaps.v
-demo.v
+-R theories MMaps
+
+theories/Utils.v
+theories/Comparisons.v
+theories/Interface.v
+theories/Facts.v
+theories/Raw.v
+theories/WeakList.v
+theories/OrdList.v
+theories/Positive.v
+theories/GenTree.v
+theories/AVL.v
+theories/AVLproofs.v
+theories/RBT.v
+theories/RBTproofs.v
+theories/MMaps.v
+theories/demo.v
diff --git a/AVL.v b/theories/AVL.v
similarity index 100%
rename from AVL.v
rename to theories/AVL.v
diff --git a/AVLproofs.v b/theories/AVLproofs.v
similarity index 100%
rename from AVLproofs.v
rename to theories/AVLproofs.v
diff --git a/Comparisons.v b/theories/Comparisons.v
similarity index 100%
rename from Comparisons.v
rename to theories/Comparisons.v
diff --git a/Facts.v b/theories/Facts.v
similarity index 100%
rename from Facts.v
rename to theories/Facts.v
diff --git a/GenTree.v b/theories/GenTree.v
similarity index 100%
rename from GenTree.v
rename to theories/GenTree.v
diff --git a/Interface.v b/theories/Interface.v
similarity index 100%
rename from Interface.v
rename to theories/Interface.v
diff --git a/MMaps.v b/theories/MMaps.v
similarity index 100%
rename from MMaps.v
rename to theories/MMaps.v
diff --git a/OrdList.v b/theories/OrdList.v
similarity index 100%
rename from OrdList.v
rename to theories/OrdList.v
diff --git a/Positive.v b/theories/Positive.v
similarity index 100%
rename from Positive.v
rename to theories/Positive.v
diff --git a/RBT.v b/theories/RBT.v
similarity index 100%
rename from RBT.v
rename to theories/RBT.v
diff --git a/RBTproofs.v b/theories/RBTproofs.v
similarity index 100%
rename from RBTproofs.v
rename to theories/RBTproofs.v
diff --git a/Raw.v b/theories/Raw.v
similarity index 100%
rename from Raw.v
rename to theories/Raw.v
diff --git a/Utils.v b/theories/Utils.v
similarity index 100%
rename from Utils.v
rename to theories/Utils.v
diff --git a/WeakList.v b/theories/WeakList.v
similarity index 100%
rename from WeakList.v
rename to theories/WeakList.v
diff --git a/demo.v b/theories/demo.v
similarity index 100%
rename from demo.v
rename to theories/demo.v

From 7ff5840bc899b133c14adbb4097bd3988f13ea2b Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Fri, 28 Oct 2022 23:34:52 +0200
Subject: [PATCH 2/6] add basic Dune build

---
 dune-project  | 3 +++
 theories/dune | 4 ++++
 2 files changed, 7 insertions(+)
 create mode 100644 dune-project
 create mode 100644 theories/dune

diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..fb7d688
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 2.5)
+(using coq 0.2)
+(name coq-mmaps)
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000..4697ee9
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,4 @@
+(coq.theory
+ (name MMaps)
+ (package coq-mmaps)
+ (synopsis "Several implementations of finite maps over arbitrary ordered types using Coq functors"))

From 9ab3dca84771218d063ba0d383954876117066ff Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sat, 29 Oct 2022 06:58:04 +0200
Subject: [PATCH 3/6] metadata reformulations

---
 README.md      | 22 ++++++++++++++++------
 coq-mmaps.opam |  9 +++++----
 meta.yml       | 23 ++++++-----------------
 3 files changed, 27 insertions(+), 27 deletions(-)

diff --git a/README.md b/README.md
index 3e7d616..fabd9d6 100644
--- a/README.md
+++ b/README.md
@@ -23,10 +23,11 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 
 
-This project contains several implementations of finite maps
-over arbitrary ordered types using Coq functors. This is an
-updated version of Coq Stdlib's FMaps. It is meant to complement
-the MSet library.
+This project contains several implementations of finite maps,
+including implementations based on AVL trees and red-black trees.
+The finite maps are parameterized on arbitrary ordered types using
+Coq functors. This is an updated version of the Coq Stdlib's FMaps
+that is meant to complement the Stdlib's MSet library.
 
 ## Meta
 
@@ -35,7 +36,7 @@ the MSet library.
 - Coq-community maintainer(s):
   - Pierre Letouzey ([**@letouzey**](https://github.com/letouzey))
   - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
-- License: [GNU Lesser General Public License v2.1](LICENSE)
+- License: [GNU Lesser General Public License v2.1 only](LICENSE)
 - Compatible Coq versions: 8.14 and later
 - Additional dependencies: none
 - Coq namespace: `MMaps`
@@ -43,7 +44,15 @@ the MSet library.
 
 ## Building and installation instructions
 
-To build and install manually, do:
+The easiest way to install the latest released version of Modular Finite Maps over Ordered Types
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
+
+```shell
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-mmaps
+```
+
+To instead build and install manually, do:
 
 ``` shell
 git clone https://github.com/coq-community/coq-mmaps.git
@@ -52,6 +61,7 @@ make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```
 
+
 ## Documentation
 
 As a starting point, you may consider [MMaps.Interface](Interface.v)
diff --git a/coq-mmaps.opam b/coq-mmaps.opam
index b584513..cc6c9b4 100644
--- a/coq-mmaps.opam
+++ b/coq-mmaps.opam
@@ -12,10 +12,11 @@ license: "LGPL-2.1-only"
 
 synopsis: "Several implementations of finite maps over arbitrary ordered types using Coq functors"
 description: """
-This project contains several implementations of finite maps
-over arbitrary ordered types using Coq functors. This is an
-updated version of Coq Stdlib's FMaps. It is meant to complement
-the MSet library."""
+This project contains several implementations of finite maps,
+including implementations based on AVL trees and red-black trees.
+The finite maps are parameterized on arbitrary ordered types using
+Coq functors. This is an updated version of the Coq Stdlib's FMaps
+that is meant to complement the Stdlib's MSet library."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]
diff --git a/meta.yml b/meta.yml
index 1256b54..0a9e3ca 100644
--- a/meta.yml
+++ b/meta.yml
@@ -9,10 +9,11 @@ action: true
 synopsis: Several implementations of finite maps over arbitrary ordered types using Coq functors
 
 description: |-
-  This project contains several implementations of finite maps
-  over arbitrary ordered types using Coq functors. This is an
-  updated version of Coq Stdlib's FMaps. It is meant to complement
-  the MSet library.
+  This project contains several implementations of finite maps,
+  including implementations based on AVL trees and red-black trees.
+  The finite maps are parameterized on arbitrary ordered types using
+  Coq functors. This is an updated version of the Coq Stdlib's FMaps
+  that is meant to complement the Stdlib's MSet library.
 
 authors:
 - name: Pierre Letouzey
@@ -29,7 +30,7 @@ opam-file-maintainer: palmskog@gmail.com
 opam-file-version: dev
 
 license:
-  fullname: GNU Lesser General Public License v2.1
+  fullname: GNU Lesser General Public License v2.1 only
   identifier: LGPL-2.1-only
 
 supported_coq_versions:
@@ -53,18 +54,6 @@ keywords:
 categories:
 - name: Computer Science/Data Types and Data Structures
 
-build: |-
-  ## Building and installation instructions
-
-  To build and install manually, do:
-
-  ``` shell
-  git clone https://github.com/coq-community/coq-mmaps.git
-  cd coq-mmaps
-  make   # or make -j <number-of-cores-on-your-machine> 
-  make install
-  ```
-
 documentation: |-
   ## Documentation
 

From 0a8c363cf2e14198cc6faa727b2337cedca8e887 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sat, 29 Oct 2022 12:18:56 +0200
Subject: [PATCH 4/6] add related publications

---
 README.md | 4 +++-
 meta.yml  | 7 +++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index fabd9d6..15cebaa 100644
--- a/README.md
+++ b/README.md
@@ -40,7 +40,9 @@ that is meant to complement the Stdlib's MSet library.
 - Compatible Coq versions: 8.14 and later
 - Additional dependencies: none
 - Coq namespace: `MMaps`
-- Related publication(s): none
+- Related publication(s):
+  - [Efficient Verified Red-Black Trees](https://www.cs.princeton.edu/~appel/papers/redblack.pdf) 
+  - [Functors for Proofs and Programs](https://hal.inria.fr/hal-00150913) doi:[10.1007/978-3-540-24725-8_26](https://doi.org/10.1007/978-3-540-24725-8_26)
 
 ## Building and installation instructions
 
diff --git a/meta.yml b/meta.yml
index 0a9e3ca..0fd1a18 100644
--- a/meta.yml
+++ b/meta.yml
@@ -15,6 +15,13 @@ description: |-
   Coq functors. This is an updated version of the Coq Stdlib's FMaps
   that is meant to complement the Stdlib's MSet library.
 
+publications:
+- pub_url: https://www.cs.princeton.edu/~appel/papers/redblack.pdf
+  pub_title: Efficient Verified Red-Black Trees
+- pub_url: https://hal.inria.fr/hal-00150913
+  pub_title: Functors for Proofs and Programs
+  pub_doi: 10.1007/978-3-540-24725-8_26
+
 authors:
 - name: Pierre Letouzey
   initial: true

From 16fd050a92c682129a8b841160fffddbba995f3b Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sun, 30 Oct 2022 07:59:34 +0100
Subject: [PATCH 5/6] coqdoc resectioning

---
 _CoqProject            |  2 +-
 theories/AVL.v         | 69 ++++++++++++++++++-------------------
 theories/AVLproofs.v   | 15 ++++----
 theories/Comparisons.v |  6 ++--
 theories/Facts.v       | 74 +++++++++++++++++++--------------------
 theories/GenTree.v     | 64 +++++++++++++++++-----------------
 theories/Interface.v   | 11 +++---
 theories/MMaps.v       |  7 ++--
 theories/OrdList.v     | 31 ++++++++---------
 theories/Positive.v    | 23 ++++++-------
 theories/RBT.v         | 78 ++++++++++++++++++++----------------------
 theories/RBTproofs.v   | 13 ++++---
 theories/Raw.v         | 10 +++---
 theories/Utils.v       |  7 ++--
 theories/WeakList.v    | 43 ++++++++++++-----------
 theories/demo.v        | 13 ++++---
 16 files changed, 231 insertions(+), 235 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 2629184..bf8166c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,8 +3,8 @@
 theories/Utils.v
 theories/Comparisons.v
 theories/Interface.v
-theories/Facts.v
 theories/Raw.v
+theories/Facts.v
 theories/WeakList.v
 theories/OrdList.v
 theories/Positive.v
diff --git a/theories/AVL.v b/theories/AVL.v
index d9e5268..b2179bb 100644
--- a/theories/AVL.v
+++ b/theories/AVL.v
@@ -1,12 +1,11 @@
+(** * Finite Modular Maps: AVL Trees *)
 
-(** * Finite Modular Maps : AVL Trees *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This module implements maps using AVL trees.
-    It follows the implementation from Ocaml's standard library.
+    It follows the implementation from OCaml's standard library.
 
     See the comments at the beginning of MSetAVL for more details.
 
@@ -27,14 +26,14 @@ Local Unset Strict Implicit.
 (* For nicer extraction, we create inductive principles only when needed *)
 Local Unset Elimination Schemes.
 
-(** * The Raw functor
-
-   Functor of pure functions + separate proofs of invariant
+(** Functor of pure functions + separate proofs of invariant
    preservation *)
 
 Module MakeRaw (Import I:Int)(K: OrderedType) <: Raw.S K.
 
-(** ** Generic trees instantiated with integer height *)
+(** ** Functions *)
+
+(** *** Generic trees instantiated with integer height *)
 
 (** We reuse a generic definition of trees where the information
     parameter is a [Int.t]. Functions like mem or fold are also
@@ -52,7 +51,7 @@ Local Notation t := (tree elt).
 Implicit Types l r m : t.
 Implicit Types e : elt.
 
-(** * Basic functions on trees: height and cardinal *)
+(** *** Basic functions on trees: height and cardinal *)
 
 Definition height (m : t) : int :=
   match m with
@@ -60,11 +59,11 @@ Definition height (m : t) : int :=
   | Node h _ _ _ _ => h
   end.
 
-(** * Singleton set *)
+(** *** Singleton set *)
 
 Definition singleton x e := Node 1 (Leaf _) x e (Leaf _).
 
-(** * Helper functions *)
+(** *** Helper functions *)
 
 (** [create l x r] creates a node, assuming [l] and [r]
     to be balanced and [|height l - height r| <= 2]. *)
@@ -110,7 +109,7 @@ Definition bal l x d r :=
     else
       create l x d r.
 
-(** * Insertion *)
+(** *** Insertion *)
 
 Fixpoint add x d m :=
   match m with
@@ -123,7 +122,7 @@ Fixpoint add x d m :=
       end
   end.
 
-(** * Extraction of minimum binding
+(** *** Extraction of minimum binding
 
   Morally, [remove_min] is to be applied to a non-empty tree
   [t = Node l x e r h]. Since we can't deal here with [assert false]
@@ -138,7 +137,7 @@ Fixpoint remove_min l x d r : t*(key*elt) :=
        (bal l' x d r, m)
   end.
 
-(** * Appending two disjoint maps of similar heights
+(** *** Appending two disjoint maps of similar heights
 
   [append t1 t2] builds the union of [t1] and [t2] assuming all keys
   of [t1] to be smaller than all keys of [t2], and
@@ -156,7 +155,7 @@ Definition append s1 s2 :=
       bal s1 x d s2'
   end.
 
-(** * Deletion *)
+(** *** Deletion *)
 
 Fixpoint remove x m := match m with
   | Leaf _ => Leaf _
@@ -168,7 +167,7 @@ Fixpoint remove x m := match m with
       end
    end.
 
-(** * join
+(** *** Join
 
     Same as [bal] but does not assume anything regarding heights of [l]
     and [r].
@@ -187,7 +186,7 @@ Fixpoint join l : key -> elt -> t -> t :=
           end
   end.
 
-(** * Splitting
+(** *** Splitting
 
     [split x m] returns a triple [(l, o, r)] where
     - [l] is the set of elements of [m] that are [< x]
@@ -207,7 +206,7 @@ Fixpoint split x m : triple := match m with
      end
  end.
 
-(** * Concatenation
+(** *** Concatenation
 
    Same as [append] but does not assume anything about heights.
 *)
@@ -221,7 +220,7 @@ Definition concat m1 m2 :=
             join m1 xd#1 xd#2 m2'
    end.
 
-(** Filter and partition *)
+(** *** Filter and partition *)
 
 Fixpoint filter (f:key->elt->bool) m :=
   match m with
@@ -249,7 +248,7 @@ Local Notation "t #l" := (t_left t) (at level 9, format "t '#l'").
 Local Notation "t #o" := (t_opt t) (at level 9, format "t '#o'").
 Local Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
 
-(** * Map with removal *)
+(** *** Map with removal *)
 
 Fixpoint mapo (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
   : t elt' :=
@@ -262,7 +261,7 @@ Fixpoint mapo (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
       end
   end.
 
-(** * Generalized merge
+(** *** Generalized merge
 
   Suggestion by B. Gregoire: a [merge] function with specialized
   arguments that allows bypassing some tree traversal. Instead of one
@@ -296,7 +295,7 @@ Fixpoint gmerge m1 m2 :=
 
 End GMerge.
 
-(** * Merge
+(** *** Merge
 
     The [merge] function of the Map interface can be implemented
     via [gmerge] and [mapo].
@@ -314,7 +313,7 @@ Definition merge : t elt -> t elt' -> t elt'' :=
 
 End Merge.
 
-(** * Correctness proofs *)
+(** ** Correctness proofs *)
 
 Include MMaps.GenTree.Props K I.
 Import Ind.
@@ -335,7 +334,7 @@ Functional Scheme split_ind := Induction for split Sort Prop.
 Functional Scheme mapo_ind := Induction for mapo Sort Prop.
 Functional Scheme gmerge_ind := Induction for gmerge Sort Prop.
 
-(** * Automation and dedicated tactics. *)
+(** *** Automation and dedicated tactics *)
 
 Local Hint Constructors tree MapsTo Bst : map.
 Local Hint Unfold Ok Bst_Ok In : map.
@@ -378,7 +377,7 @@ Variable elt:Type.
 Implicit Types x y : K.t.
 Implicit Types m r : t elt.
 
-(** * Helper functions *)
+(** *** Helper functions *)
 
 #[export] Instance create_ok l x e r `{!Ok l, !Ok r} :
  l < x -> x < r -> Ok (create l x e r).
@@ -446,7 +445,7 @@ Proof.
  unfold singleton. autok.
 Qed.
 
-(** * Insertion *)
+(** *** Insertion *)
 
 Lemma add_in m x y e :
  y ∈ (add x e m) <-> y == x \/ y ∈ m.
@@ -522,7 +521,7 @@ Proof.
  rewrite app_ass. f_equal. simpl. f_equal. intuition.
 Qed.
 
-(** * Extraction of minimum binding *)
+(** *** Extraction of minimum binding *)
 
 Definition RemoveMin m res :=
  match m with
@@ -623,7 +622,7 @@ Proof.
  now rewrite (IH _ R).
 Qed.
 
-(** * Merging two trees *)
+(** *** Merging two trees *)
 
 Ltac factor_remove_min m R := match goal with
  | h:int, H:remove_min ?l ?x ?e ?r = ?p |- _ =>
@@ -657,7 +656,7 @@ Proof.
  - now apply (remove_min_gt R).
 Qed.
 
-(** * Deletion *)
+(** *** Deletion *)
 
 Lemma remove_in m x y `{!Ok m} :
  y ∈ remove x m <-> ~ y == x /\ y ∈ m.
@@ -699,7 +698,7 @@ Proof.
  - rewrite bal_find by autok. simpl. case K.compare_spec; auto.
 Qed.
 
-(** * join *)
+(** *** Join *)
 
 Lemma join_in l x d r y :
  y ∈ (join l x d r) <-> y == x \/ y ∈ l \/ y ∈ r.
@@ -773,7 +772,7 @@ Proof.
    now rewrite Hrl, create_bindings, app_ass by (ok; intuition).
 Qed.
 
-(** * split *)
+(** *** Split *)
 
 Lemma split_in_l0 m x y : y ∈ (split x m)#l -> y ∈ m.
 Proof.
@@ -855,7 +854,7 @@ Proof.
    simpl; repeat case K.compare_spec; trivial; order.
 Qed.
 
-(** * Concatenation *)
+(** *** Concatenation *)
 
 Lemma concat_in m1 m2 y :
  y ∈ (concat m1 m2) <-> y ∈ m1 \/ y ∈ m2.
@@ -916,7 +915,7 @@ Proof.
    + apply create_ok; eauto with *. now apply (remove_min_gt R).
 Qed.
 
-(** Filter and partition *)
+(** *** Filter and partition *)
 
 Lemma filter_in_inv f (m:t elt) x : x ∈ filter f m -> x ∈ m.
 Proof.
@@ -1219,7 +1218,7 @@ Qed.
 End Merge.
 End MakeRaw.
 
-(** * Encapsulation
+(** ** Encapsulation
 
    Now, in order to really provide a functor implementing [S], we need
    to encapsulate everything into a type of binary search trees. *)
diff --git a/theories/AVLproofs.v b/theories/AVLproofs.v
index 7e23f32..8f5bac7 100644
--- a/theories/AVLproofs.v
+++ b/theories/AVLproofs.v
@@ -1,9 +1,8 @@
+(** * Finite Modular Maps: AVL Proofs *)
 
-(** * Finite Modular Maps : AVL Proofs *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This is a complement to [MMaps.AVL], proving the AVL balancing
     invariants for the code in [MMaps.AVL], and hence the logarithmic
@@ -31,7 +30,7 @@ Ltac mysubst :=
    | _ => idtac
  end.
 
-(** * AVL trees *)
+(** ** AVL trees *)
 
 (** [avl s] : [s] is a properly balanced AVL tree,
     i.e. for any node the heights of the two children
@@ -48,7 +47,7 @@ Class Avl elt (t:tree elt) : Prop := mkAvl : avl t.
 
 #[export] Instance avl_Avl elt (s:tree elt) (Hs : avl s) : Avl s := Hs.
 
-(** * Automation and dedicated tactics *)
+(** ** Automation and dedicated tactics *)
 
 Local Hint Constructors avl : map.
 
@@ -75,7 +74,7 @@ Ltac inv_avl' :=
     inversion_clear H; avl2Avl
   end.
 
-(** * AVL trees have indeed logarithmic depth *)
+(** ** AVL trees have logarithmic depth *)
 
 Module LogDepth.
 
@@ -285,7 +284,7 @@ Proof.
 Qed.
 Local Hint Resolve avl_node : map.
 
-(** * The AVL invariant is preserved by set operations *)
+(** ** The AVL invariant is preserved by set operations *)
 
 (** empty *)
 
diff --git a/theories/Comparisons.v b/theories/Comparisons.v
index e46ed5c..bb3950e 100644
--- a/theories/Comparisons.v
+++ b/theories/Comparisons.v
@@ -1,9 +1,11 @@
+(** * Finite Modular Maps: comparison utilities *)
+
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 From Coq Require Import List.
 Import ListNotations.
 
-(** * Some complements on [comparison] *)
-
 Set Implicit Arguments.
 
 (** lexicographic product, defined using a notation to keep things lazy *)
diff --git a/theories/Facts.v b/theories/Facts.v
index 6b051ce..3632ed4 100644
--- a/theories/Facts.v
+++ b/theories/Facts.v
@@ -1,9 +1,8 @@
+(** * Finite Modular Maps: Functors of Properties *)
 
-(** * Finite Modular Maps : Functors of Properties *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This functor derives additional facts from [MMaps.Interface.S]. These
   facts are mainly the specifications of [MMaps.Interface.S] written using
@@ -14,10 +13,11 @@ From Coq Require Import Bool Equalities Orders OrdersFacts OrdersLists.
 From Coq Require OrdersAlt.
 From Coq Require Import Morphisms Permutation SetoidPermutation.
 From MMaps Require Import Utils Comparisons Interface.
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Properties that are common to weak maps and ordered maps.
+(** ** Properties that are common to weak maps and ordered maps
 
     Thanks to subtyping, this functor can also be applied to
     [(K:OrderedType)(M:S K)].
@@ -77,7 +77,7 @@ Qed.
 Notation in_find_iff := in_find (only parsing).
 Notation not_find_in_iff := not_in_find (only parsing).
 
-(** * [Equal] and [Eqdom] are setoid equalities. *)
+(** *** Equal and Eqdom are setoid equalities *)
 
 Infix "==" := Equal (at level 30).
 
@@ -192,7 +192,7 @@ Qed.
 
 (* Later: compatibility for cardinal, fold, map, mapi... *)
 
-(** ** Earlier specifications (cf. FMaps) *)
+(** *** Earlier specifications (cf. FMaps) *)
 
 Section OldSpecs.
 Variable elt: Type.
@@ -414,7 +414,7 @@ Proof. apply merge_spec2. Qed.
 #[export] Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 : map.
 #[export] Hint Resolve remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 : map.
 
-(** ** Specifications written using equivalences *)
+(** *** Specifications written using equivalences *)
 
 Section IffSpec.
 Variable elt: Type.
@@ -690,7 +690,7 @@ Ltac map_iff :=
   rewrite map_mapsto_iff || rewrite map_in_iff ||
   rewrite mapi_in_iff)).
 
-(** ** Specifications via the reflect predicate *)
+(** *** Specifications via the reflect predicate *)
 
 Lemma is_empty_spec' {elt}(m:t elt) : reflect (Empty m) (is_empty m).
 Proof.
@@ -702,7 +702,7 @@ Proof.
  apply iff_reflect. apply mem_in_iff.
 Qed.
 
-(** ** Specifications written using boolean predicates *)
+(** *** Specifications written using boolean predicates *)
 
 Section BoolSpec.
 
@@ -1013,7 +1013,7 @@ intro k. rewrite eq_option_alt. intro e.
 rewrite <- 2 find_mapsto_iff; auto.
 Qed.
 
-(** * Relations between [Equal], [Eqdom], [Equiv] and [Equivb]. *)
+(** *** Relations between Equal, Eqdom, Equiv and Equivb *)
 
 (** First, [Equal] is [Equiv] with Leibniz on elements. *)
 
@@ -1089,7 +1089,7 @@ Qed.
 
 End Equalities.
 
-(** * Results about [fold], [bindings], induction principles... *)
+(** Results about fold, bindings, and induction principles *)
 
 Section Elt.
   Variable elt:Type.
@@ -1154,7 +1154,7 @@ Section Elt.
   change (NoDupA eqk (rev l)). apply NoDupA_rev; auto using eqk_equiv.
   Qed.
 
-  (** * Bindings *)
+  (** *** Bindings *)
 
   Lemma in_bindings_iff m x :
     In x m <-> exists e, InA eqk (x,e) (bindings m).
@@ -1199,7 +1199,7 @@ Section Elt.
   rewrite <-bindings_Empty; apply empty_1.
   Qed.
 
-  (** * Conversions between maps and association lists. *)
+  (** *** Conversions between maps and association lists *)
 
   Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W :=
    fun p => f (fst p) (snd p).
@@ -1251,8 +1251,6 @@ Section Elt.
   apply bindings_3w.
   Qed.
 
-  (** * Fold *)
-
   (** Alternative specification via [fold_right] *)
 
   Lemma fold_spec_right m {A}(i:A)(f : key -> elt -> A -> A) :
@@ -1261,7 +1259,7 @@ Section Elt.
    rewrite fold_1. symmetry. apply fold_left_rev_right.
   Qed.
 
-  (** ** Induction principles about fold contributed by S. Lescuyer *)
+  (** *** Induction principles about fold contributed by S. Lescuyer *)
 
   (** In the following lemma, the step hypothesis is deliberately restricted
       to the precise map m we are considering. *)
@@ -1411,7 +1409,7 @@ Section Elt.
 
   Section Fold_More.
 
-  (** ** Additional properties of fold *)
+  (** *** Additional properties of fold *)
 
   (** When a function [f] is compatible and allows transpositions, we can
       compute [fold f] in any order. *)
@@ -1526,7 +1524,7 @@ Section Elt.
 
   End Fold_More.
 
-  (** ** Special case of a fold only on keys *)
+  (** *** Special case of a fold only on keys *)
 
   Section Fold_Keys.
   Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
@@ -1598,7 +1596,7 @@ Section Elt.
 
   End Fold_Keys.
 
-  (** * Cardinal *)
+  (** *** Cardinal *)
 
   Lemma cardinal_fold m :
    cardinal m = fold (fun _ _ => S) m 0.
@@ -1751,7 +1749,7 @@ Section Elt.
   exists x, e. now left.
   Qed.
 
-  (** * Properties about filter, partition, for_all, exists_ *)
+  (** *** Properties about filter, partition, for_all, and exists_ *)
 
   (** First, alternative formulations, e.g. based on fold,
       or on filter for the other operations *)
@@ -1956,7 +1954,7 @@ Section Elt.
   Definition partition_dom (f : key -> bool) := partition (fun k e => f k).
   Definition partition_range (f : elt -> bool) := partition (fun k => f).
 
-  (** * Extra predicates on maps : Disjoint and Partition *)
+  (** *** Extra predicates on maps: Disjoint and Partition *)
 
   Definition Disjoint m m' := forall k, ~(In k m /\ In k m').
 
@@ -1964,14 +1962,14 @@ Section Elt.
     Disjoint m1 m2 /\
     (forall k e, MapsTo k e m <-> MapsTo k e m1 \/ MapsTo k e m2).
 
-   #[export] Instance Disjoint_m : Proper (Eqdom ==> Eqdom ==> iff) Disjoint.
+  #[export] Instance Disjoint_m : Proper (Eqdom ==> Eqdom ==> iff) Disjoint.
   Proof.
   intros m1 m1' Hm1 m2 m2' Hm2. unfold Disjoint. split; intros.
   rewrite <- Hm1, <- Hm2; auto.
   rewrite Hm1, Hm2; auto.
   Qed.
 
-   #[export] Instance Partition_m :
+  #[export] Instance Partition_m :
    Proper (Equal ==> Equal ==> Equal ==> iff) Partition.
   Proof.
   intros m1 m1' Hm1 m2 m2' Hm2 m3 m3' Hm3. unfold Partition.
@@ -2170,7 +2168,7 @@ Section Elt.
     rewrite <- not_mem_in_iff. destruct Hm as (Hm,->). firstorder.
   Qed.
 
-  (** * Emulation of some functions lacking in the interface *)
+  (** *** Emulation of some functions lacking in the interface *)
 
   (** [update] now mimics the one of OCaml : [update x f m] returns a map
       containing the same bindings as m, except for the binding of
@@ -2232,7 +2230,7 @@ Section Elt.
   destruct f; [apply add_spec2 | apply remove_spec2]; auto.
   Qed.
 
-   #[export] Instance update_m : Proper (K.eq==>(eq==>eq)==>Equal==>Equal) update.
+  #[export] Instance update_m : Proper (K.eq==>(eq==>eq)==>Equal==>Equal) update.
   Proof.
   intros x x' Hx f f' Hf m m' Hm. unfold update.
   rewrite <- Hx. rewrite <- Hm at 1. rewrite <- (Hf (find x m)) by auto.
@@ -2253,7 +2251,7 @@ Section Elt.
     destruct o1, o2; auto. apply Hf; auto.
   Qed.
 
-   #[export] Instance union_m :
+  #[export] Instance union_m :
     Proper ((K.eq==>eq==>eq==>eq)==>Equal==>Equal==>Equal) union.
   Proof.
   intros f f' Hf m1 m1' Hm1 m2 m2' Hm2. unfold union.
@@ -2374,7 +2372,7 @@ Section Elt.
 
 End Properties.
 
-(** * Properties specific to maps with ordered keys *)
+(** ** Properties specific to maps with ordered keys *)
 
 Module OrdProperties (K:OrderedType)(M:S K).
  Module Import F := OrderedTypeFacts K.
@@ -2685,7 +2683,7 @@ Module OrdProperties (K:OrderedType)(M:S K).
   - intros [x|] [y|] [z|]; simpl; eauto; try easy. now transitivity y.
   Qed.
 
-   #[export] Instance min_elt_m : Proper (Equal ==> optrel eqke) min_elt.
+  #[export] Instance min_elt_m : Proper (Equal ==> optrel eqke) min_elt.
   Proof.
   intros m m' E. unfold min_elt.
   apply bindings_Equal_eqlistA in E.
@@ -2693,7 +2691,7 @@ Module OrdProperties (K:OrderedType)(M:S K).
   now destruct x as (k,e), x' as (k',e').
   Qed.
 
-   #[export] Instance min_elt_m' : Proper (Eqdom ==> optrel eqk) min_elt.
+  #[export] Instance min_elt_m' : Proper (Eqdom ==> optrel eqk) min_elt.
   Proof.
   intros m m' E. unfold min_elt.
   apply bindings_Eqdom_eqlistA in E.
@@ -2775,13 +2773,13 @@ Module OrdProperties (K:OrderedType)(M:S K).
   destruct l, l'; simpl; auto. inversion H1. inversion H1.
   Qed.
 
-   #[export] Instance max_elt_m : Proper (Equal ==> optrel eqke) max_elt.
+  #[export] Instance max_elt_m : Proper (Equal ==> optrel eqke) max_elt.
   Proof.
   intros m m' E. unfold max_elt.
   apply bindings_Equal_eqlistA in E. now rewrite E.
   Qed.
 
-   #[export] Instance max_elt_m' : Proper (Eqdom ==> optrel eqk) max_elt.
+  #[export] Instance max_elt_m' : Proper (Eqdom ==> optrel eqk) max_elt.
   Proof.
   intros m m' E. unfold max_elt.
   apply bindings_Eqdom_eqlistA in E. now rewrite E.
@@ -2845,7 +2843,7 @@ Module OrdProperties (K:OrderedType)(M:S K).
 
   Section Fold_properties.
 
-   #[export] Instance fold_m {A}(eqA:A->A->Prop)(st:Equivalence eqA) :
+  #[export] Instance fold_m {A}(eqA:A->A->Prop)(st:Equivalence eqA) :
    Proper ((K.eq==>eq==>eqA==>eqA)==>Equal==>eqA==>eqA) (@fold elt A).
   Proof.
   intros f f' Hf m m' Hm i i' Hi.
@@ -2909,7 +2907,7 @@ Module OrdProperties (K:OrderedType)(M:S K).
     rewrite ?compare_eq_iff, ?compare_lt_iff,  ?compare_gt_iff; order.
   Qed.
 
-   #[export] Instance Kcompare_symtrans : SymTrans K.compare.
+  #[export] Instance Kcompare_symtrans : SymTrans K.compare.
   Proof.
    split. exact F.compare_antisym. exact Kcompare_trans.
   Qed.
@@ -2948,7 +2946,7 @@ Module OrdProperties (K:OrderedType)(M:S K).
   Variable cmp : elt -> elt -> comparison.
   Context `(!SymTrans cmp).
 
-   #[export] Instance compare_symtrans : SymTrans (compare cmp).
+  #[export] Instance compare_symtrans : SymTrans (compare cmp).
   Proof.
   constructor.
   - intros x y. rewrite !compare_spec; apply sym; eauto with *.
@@ -2965,7 +2963,7 @@ Module OrdProperties (K:OrderedType)(M:S K).
   rewrite sym, CompOpp_iff in E. simpl in E. congruence.
   Qed.
 
-   #[export] Instance eq_equiv : Equivalence eq.
+  #[export] Instance eq_equiv : Equivalence eq.
   Proof.
   split.
   - intro x. apply compare_refl.
@@ -2973,14 +2971,14 @@ Module OrdProperties (K:OrderedType)(M:S K).
   - intros x y z. apply tra.
   Qed.
 
-   #[export] Instance lt_strorder : StrictOrder lt.
+  #[export] Instance lt_strorder : StrictOrder lt.
   Proof.
   split.
   - intros x. red. unfold lt. now rewrite compare_refl.
   - intros x y z. apply tra.
   Qed.
 
-   #[export] Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
+  #[export] Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
   Proof.
   intros x x' E y y' E'. unfold lt,eq in *. split; intros <-.
   - symmetry.
diff --git a/theories/GenTree.v b/theories/GenTree.v
index c56c85b..a7d11fe 100644
--- a/theories/GenTree.v
+++ b/theories/GenTree.v
@@ -1,6 +1,9 @@
-(** * MSets.GenTree : maps via generic trees
+(** * Finite Modular Maps: Generic Trees *)
 
-    This module factorizes common parts in implementations
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
+    License: LGPL-2.1-only, see file LICENSE. *)
+
+(** This module factorizes common parts in implementations
     of finite maps as AVL trees and as Red-Black trees. The nodes
     of the trees defined here include an generic information
     parameter, that will be the height in AVL trees and the color
@@ -41,7 +44,7 @@ Module Type InfoTyp.
  Parameter t : Set.
 End InfoTyp.
 
-(** * Ops : the pure functions *)
+(** ** Ops: the pure functions *)
 
 Module Type Ops (K:OrderedType)(Info:InfoTyp).
 
@@ -51,7 +54,7 @@ Section Elt.
 
 Variable elt : Type.
 
-(** * Trees *)
+(** *** Trees *)
 
 Inductive tree  : Type :=
 | Leaf : tree
@@ -59,7 +62,7 @@ Inductive tree  : Type :=
 
 Definition t := tree.
 
-(** ** The empty map and emptyness test *)
+(** *** The empty map and emptiness test *)
 
 Definition empty := Leaf.
 
@@ -69,7 +72,7 @@ Definition is_empty t :=
  | _ => false
  end.
 
-(** ** Membership test *)
+(** *** Membership test *)
 
 (** The [mem] function is deciding membership. It exploits the
     binary search tree invariant to achieve logarithmic complexity. *)
@@ -96,7 +99,7 @@ Fixpoint find x m : option elt :=
        end
    end.
 
-(** ** Minimal, maximal, arbitrary bindings *)
+(** *** Minimal, maximal, arbitrary bindings *)
 
 Fixpoint min_binding (t : tree) : option (key * elt) :=
  match t with
@@ -114,7 +117,7 @@ Fixpoint max_binding (t : tree) : option (key * elt) :=
 
 Definition choose := min_binding.
 
-(** ** Iteration on elements *)
+(** *** Iteration on elements *)
 
 Fixpoint fold {A: Type} (f: key -> elt -> A -> A) (t: tree) (base: A) : A :=
   match t with
@@ -156,7 +159,7 @@ Fixpoint mindepth s :=
  | Node _ l _ _ r => S (min (mindepth l) (mindepth r))
  end.
 
-(** ** Testing universal or existential properties. *)
+(** *** Testing universal or existential properties *)
 
 (** We do not use the standard boolean operators of Coq,
     but lazy ones. *)
@@ -171,7 +174,7 @@ Fixpoint exists_ (f:key->elt->bool) s := match s with
   | Node _ l x e r => f x e ||| exists_ f l ||| exists_ f r
 end.
 
-(** ** Comparison of trees *)
+(** *** Comparison of trees *)
 
 (** The algorithm here has been suggested by Xavier Leroy,
     and transformed into c.p.s. by Benjamin Grégoire.
@@ -182,8 +185,6 @@ end.
     should be almost as efficient after extraction.
 *)
 
-(** * Comparison *)
-
 (** Enumeration of the elements of a tree. This corresponds
     to the "samefringe" notion in the litterature. *)
 
@@ -265,7 +266,7 @@ Definition compare m1 m2 :=
 
 End Elt.
 
-(** ** Map *)
+(** *** Map *)
 
 Fixpoint map {elt elt'}(f : elt -> elt')(m : t elt) : t elt' :=
   match m with
@@ -273,7 +274,7 @@ Fixpoint map {elt elt'}(f : elt -> elt')(m : t elt) : t elt' :=
    | Node h l x d r => Node h (map f l) x (f d) (map f r)
   end.
 
-(* ** Mapi *)
+(** *** Mapi *)
 
 Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
   match m with
@@ -283,7 +284,7 @@ Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
 
 End Ops.
 
-(** * Props : correctness proofs of these generic operations *)
+(** ** Props: correctness proofs for the generic operations *)
 
 Module Type Props (K:OrderedType)(Info:InfoTyp)(Import M:Ops K Info).
 
@@ -298,7 +299,7 @@ Local Infix "<" := lessthan.
 
 #[export] Instance lt_key_key : LessThan K.t K.t := K.lt.
 
-(** ** Occurrence in a tree *)
+(** *** Occurrence in a tree *)
 
 Module Ind. (* Module allowing a "Definition" of MapsTo below. *)
 
@@ -326,7 +327,7 @@ Definition Equivb elt cmp := @Equiv elt (Cmp cmp).
 Definition AllKeys elt (P:key->Prop) (m : t elt) :=
  forall x, x ∈ m -> P x.
 
-(** ** Binary search trees *)
+(** *** Binary search trees *)
 
 (** Strict order between keys and trees:
     [x < m] when [x] is strictly smaller than any key in [m].
@@ -358,7 +359,7 @@ Module L := MMaps.OrdList.MakeRaw K.
 
 Scheme tree_ind := Induction for tree Sort Prop.
 
-(** * Automation and dedicated tactics. *)
+(** *** Automation and dedicated tactics *)
 
 Local Hint Constructors tree MapsTo Bst : map.
 Local Hint Unfold Ok In : map.
@@ -438,9 +439,9 @@ Arguments Ok {elt} m.
 Arguments Equal {elt} m m'.
 Arguments Eqdom {elt} m m'.
 
- #[export] Instance Equal_equiv {elt} : Equivalence (@Equal elt).
+#[export] Instance Equal_equiv {elt} : Equivalence (@Equal elt).
 Proof. split; congruence. Qed.
- #[export] Instance Eqdom_equiv {elt} : Equivalence (@Eqdom elt).
+#[export] Instance Eqdom_equiv {elt} : Equivalence (@Eqdom elt).
 Proof.
  split; try firstorder. intros x y z E E' k. now rewrite (E k), (E' k).
 Qed.
@@ -465,7 +466,7 @@ Proof.
 Qed.
 Local Hint Immediate mapsto_eq : map.
 
- #[export] Instance MapsTo_compat {elt} :
+#[export] Instance MapsTo_compat {elt} :
   Proper (K.eq==>Logic.eq==>Logic.eq==>iff) (@MapsTo elt).
 Proof.
  split; subst; now apply mapsto_eq.
@@ -483,7 +484,7 @@ Proof.
  intuition_m; subst; auto with map.
 Qed.
 
- #[export] Instance in_compat {elt} :
+#[export] Instance in_compat {elt} :
   Proper (K.eq==>Logic.eq==>iff) (@In elt).
 Proof.
  intros x x' E m m' <-.
@@ -553,7 +554,7 @@ Proof.
  apply allkeys_node with (P := fun z => z < x). now intros ? ? ->.
 Qed.
 
- #[export] Instance above_m {elt} :
+#[export] Instance above_m {elt} :
   Proper (@Eqdom elt ==> K.eq ==> iff) lessthan.
 Proof.
  intros until 2. apply allkeys_m; auto. split; F.order.
@@ -570,7 +571,7 @@ Proof.
  apply allkeys_node. now intros ? ? ->.
 Qed.
 
- #[export] Instance below_m {elt} :
+#[export] Instance below_m {elt} :
   Proper (K.eq ==> @Eqdom elt ==> iff) lessthan.
 Proof.
  intros until 2. apply allkeys_m; auto. split; F.order.
@@ -651,7 +652,6 @@ Proof.
  intros H; repeat split; intros y IN; now specialize (H y IN).
 Qed.
 
-
 (** Bst is decidable *)
 
 #[export] Instance Bst_Ok {elt} (m : t elt) (B : Bst m) : Ok m := B.
@@ -726,7 +726,7 @@ Section Elt.
 Variable elt:Type.
 Implicit Types m r : t elt.
 
-(** * Membership *)
+(** *** Membership *)
 
 Lemma find_1 m x e `{!Ok m} : m@x ↦ e -> find x m = Some e.
 Proof.
@@ -811,7 +811,7 @@ Proof.
  - invok. rewrite in_node. case K.compare_spec; intuition; order.
 Qed.
 
-(** * Empty map *)
+(** *** Empty map *)
 
  #[export] Instance empty_ok : Ok (empty elt).
 Proof.
@@ -823,7 +823,7 @@ Proof.
  reflexivity.
 Qed.
 
-(** * Emptyness test *)
+(** *** Emptiness test *)
 
 Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None.
 Proof.
@@ -831,7 +831,7 @@ Proof.
  intros H. specialize (H x). now rewrite F.compare_refl in H.
 Qed.
 
-(** * Elements *)
+(** *** Elements *)
 
 Definition eq_key : (key*elt) -> (key*elt) -> Prop := @O.eqk elt.
 Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @O.eqke elt.
@@ -966,7 +966,7 @@ Proof.
    try apply in_bindings in INl; try apply in_bindings in INr; order.
 Qed.
 
-(** * Fold *)
+(** *** Fold *)
 
 Definition fold' {A} (f : key -> elt -> A -> A) m :=
   L.fold f (bindings m).
@@ -991,7 +991,7 @@ Proof.
  rewrite fold_equiv. unfold fold'. now rewrite L.fold_spec.
 Qed.
 
-(** * For_all / exists *)
+(** *** For_all and exists *)
 
 Lemma for_all_spec (f:key->elt->bool) m :
   for_all f m = List.forallb (fun '(k,e) => f k e) (bindings m).
@@ -1011,7 +1011,7 @@ rewrite <- !orb_lazy_alt, orb_assoc, (orb_comm (f _ _)).
 f_equal; auto. f_equal; auto.
 Qed.
 
-(** * Comparison *)
+(** *** Comparison *)
 
 (** [flatten_e e] returns the list of bindings of the enumeration [e]
     i.e. the list of bindings actually compared *)
diff --git a/theories/Interface.v b/theories/Interface.v
index ae681d9..42d7de8 100644
--- a/theories/Interface.v
+++ b/theories/Interface.v
@@ -1,12 +1,12 @@
+(** * Finite Modular Maps: Main Interface *)
 
-(** * Finite Modular Maps : Main Interface *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 From Coq Require Export Bool Equalities Orders SetoidList.
 From MMaps Require Import Comparisons.
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -252,8 +252,7 @@ Module Type WS (K : DecidableType).
  End MapsSpecs.
 End WS.
 
-
-(** ** Maps on ordered keys. *)
+(** ** Maps on ordered keys *)
 
 Module Type S (K : OrderedType).
  Include WS K.
diff --git a/theories/MMaps.v b/theories/MMaps.v
index e9578e1..7dab2af 100644
--- a/theories/MMaps.v
+++ b/theories/MMaps.v
@@ -1,9 +1,8 @@
+(** * Finite Modular Maps: Exports *)
 
-(** * Finite Modular Maps *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 From Coq Require Export Orders OrdersEx OrdersAlt Equalities.
 From MMaps Require Export Interface Facts WeakList OrdList Positive.
diff --git a/theories/OrdList.v b/theories/OrdList.v
index f824d95..9c25973 100644
--- a/theories/OrdList.v
+++ b/theories/OrdList.v
@@ -1,9 +1,8 @@
+(** * Finite Modular Maps: Ordered Lists *)
 
-(** * Finite Modular Maps : Ordered Lists *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This file proposes an implementation of the interface
     [MMaps.Interface.S] using lists of pairs ordered (increasing)
@@ -97,7 +96,7 @@ Qed.
 Lemma isok_Ok (m:t elt) : isok m = true -> Ok m.
 Proof. apply isok_spec. Qed.
 
-(** * [find] *)
+(** ** find *)
 
 Fixpoint find (k:key) (m: t elt) : option elt :=
  match m with
@@ -126,7 +125,7 @@ Proof.
      intros [(E,<-)|IN]; trivial. MX.order.
 Qed.
 
-(** * [mem] *)
+(** ** mem *)
 
 Fixpoint mem (k : key) (m : t elt) : bool :=
  match m with
@@ -153,7 +152,7 @@ Proof.
      MX.order.
 Qed.
 
-(** * [empty] *)
+(** ** empty *)
 
 Definition empty : t elt := nil.
 
@@ -167,7 +166,7 @@ Proof.
  unfold empty; autok.
 Qed.
 
-(** * [is_empty] *)
+(** ** is_empty *)
 
 Definition is_empty (l : t elt) : bool := if l then true else false.
 
@@ -178,7 +177,7 @@ Proof.
  intros H. specialize (H k). now rewrite compare_refl in H.
 Qed.
 
-(** * [add] *)
+(** ** add *)
 
 Fixpoint add (k : key) (x : elt) (s : t elt) : t elt :=
  match s with
@@ -238,7 +237,7 @@ Proof.
    apply Inf_eq with (y,v); auto.
 Qed.
 
-(** * [remove] *)
+(** ** remove *)
 
 Fixpoint remove (k : key) (s : t elt) : t elt :=
  match s with
@@ -303,7 +302,7 @@ Proof.
  constructor; autok.
 Qed.
 
-(** * [bindings] *)
+(** ** bindings *)
 
 Definition bindings (m: t elt) := m.
 
@@ -323,7 +322,7 @@ Proof.
  now apply Sort_NoDupA.
 Qed.
 
-(** * [singleton] *)
+(** ** singleton *)
 
 Definition singleton k (e:elt) : t elt := (k,e)::nil.
 
@@ -335,7 +334,7 @@ Proof.
  constructor; auto.
 Qed.
 
-(** * [fold] *)
+(** ** fold *)
 
 Fixpoint fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc:A) :  A :=
   match m with
@@ -349,7 +348,7 @@ Proof.
  induction m as [|(k,e) m IH]; simpl; auto.
 Qed.
 
-(** * [equal] *)
+(** ** equal *)
 
 Fixpoint equal (cmp:elt->elt->bool)(m m' : t elt) : bool :=
   match m, m' with
@@ -456,7 +455,7 @@ Qed.
 
 Variable elt':Type.
 
-(** * [map] and [mapi] *)
+(** ** map and mapi *)
 
 Definition map (f:elt -> elt') (m:t elt) : t elt' :=
   List.map (fun '(k,e) => (k,f e)) m.
@@ -517,7 +516,7 @@ Qed.
 End Elt2.
 Section Elt3.
 
-(** * [merge] *)
+(** ** merge *)
 
 Variable elt elt' elt'' : Type.
 Variable f : key -> option elt -> option elt' -> option elt''.
diff --git a/theories/Positive.v b/theories/Positive.v
index f2f166b..ff90232 100644
--- a/theories/Positive.v
+++ b/theories/Positive.v
@@ -1,17 +1,8 @@
+(** * Finite Modular Maps: Implementation for Positive Keys *)
 
-(** * Finite Modular Maps : Implementation for Positive Keys *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
-
-From Coq Require Import Bool PeanoNat BinPos Orders OrdersEx OrdersLists.
-From MMaps Require Import Utils Comparisons Interface.
-
-Set Implicit Arguments.
-Local Open Scope lazy_bool_scope.
-Local Open Scope positive_scope.
-Local Unset Elimination Schemes.
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This file is an adaptation to the [MMaps] framework of a work by
   Xavier Leroy and Sandrine Blazy (used for building certified compilers).
@@ -21,6 +12,14 @@ Local Unset Elimination Schemes.
   compression is implemented, and that the current file is simple enough to be
   self-contained. *)
 
+From Coq Require Import Bool PeanoNat BinPos Orders OrdersEx OrdersLists.
+From MMaps Require Import Utils Comparisons Interface.
+
+Set Implicit Arguments.
+Local Open Scope lazy_bool_scope.
+Local Open Scope positive_scope.
+Local Unset Elimination Schemes.
+
 (** Reverses the positive [y] and concatenate it with [x] *)
 
 Fixpoint rev_append (y x : positive) : positive :=
diff --git a/theories/RBT.v b/theories/RBT.v
index 2ab0360..29ccac0 100644
--- a/theories/RBT.v
+++ b/theories/RBT.v
@@ -1,12 +1,11 @@
+(** * Finite Modular Maps: Red-Black Trees *)
 
-(** * Finite Modular Maps : Red-Black Trees *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This module implements finite maps using Red-Black trees.
-    This code is based on Coq [MSetRBT.v], due initially to
+    This code is based on [MSetRBT.v] in Coq's Stdlib, due initially to
     Andrew W. Appel, 2011. See initial comment at the beginning
     of [MSetRBT.v].
 
@@ -39,14 +38,14 @@ Module Color.
  Definition t := color.
 End Color.
 
-(** * The Raw functor
-
-   Functor of pure functions + separate proofs of invariant
+(** Functor of pure functions + separate proofs of invariant
    preservation *)
 
 Module MakeRaw (K: OrderedType) <: Raw.S K.
 
-(** ** Generic trees instantiated with Red/Black colors *)
+(** ** Functions *)
+
+(** *** Generic trees instantiated with Red/Black colors *)
 
 (** We reuse a generic definition of trees where the information
     parameter is a [Color.t]. Functions like mem or fold are also
@@ -66,12 +65,12 @@ Local Notation t := (tree elt).
 Implicit Types l r m : t.
 Implicit Types e : elt.
 
-(** ** Basic tree *)
+(** *** Basic tree *)
 
 Definition singleton (k : key) (v : elt) : t :=
   Node Black Leaf k v Leaf.
 
-(** ** Changing root color *)
+(** *** Changing root color *)
 
 Definition makeBlack m : t :=
  match m with
@@ -85,7 +84,7 @@ Definition makeRed m : t :=
  | Node _ a x v b => Rd a x v b
  end.
 
-(** ** Balancing *)
+(** *** Balancing *)
 
 (** We adapt when one side is not a true red-black tree.
     Both sides have the same black depth. *)
@@ -140,7 +139,7 @@ Definition rbalS l k vk r :=
    end
  end.
 
-(** ** Insertion *)
+(** *** Insertion *)
 
 Fixpoint ins x vx s :=
  match s with
@@ -163,7 +162,7 @@ Fixpoint ins x vx s :=
 
 Definition add x vx s := makeBlack (ins x vx s).
 
-(** ** Deletion *)
+(** *** Deletion *)
 
 Fixpoint append (l:t) : t -> t :=
  match l with
@@ -213,7 +212,7 @@ Fixpoint del x m : t :=
 
 Definition remove x m := makeBlack (del x m).
 
-(** ** Tree-ification
+(** *** Tree-ification
 
     We rebuild a tree of size [if pred then n-1 else n] as soon
     as the list [l] has enough elements *)
@@ -261,7 +260,7 @@ Definition treeify (l:klist elt) :=
 
 End Elt.
 
-(** * Map with removal *)
+(** *** Map with removal *)
 
 Definition ocons {A B} (a:A) (o:option B) (l:list (A*B)) :=
  match o with
@@ -284,7 +283,7 @@ Definition mapo (m : t elt) : t elt' :=
 
 End Mapo.
 
-(** * Merge *)
+(** *** Merge *)
 
 Section Merge.
 Variable elt elt' elt'' : Type.
@@ -312,7 +311,7 @@ Definition merge (m1 : t elt) (m2 : t elt') : t elt'' :=
 
 End Merge.
 
-(** * Correctness proofs *)
+(** ** Correctness proofs *)
 
 Include MMaps.GenTree.Props K Color.
 Import Ind.
@@ -355,26 +354,26 @@ Implicit Types m : t elt.
 Implicit Types k x y : key.
 Implicit Types v vx vy : elt.
 
-(** ** Singleton set *)
+(** *** Singleton set *)
 
 Lemma singleton_spec x (e:elt) : bindings (singleton x e) = (x,e)::nil.
 Proof.
  unfold singleton. now rewrite bindings_node.
 Qed.
 
- #[export] Instance singleton_ok x vx : Ok (singleton x vx).
+#[export] Instance singleton_ok x vx : Ok (singleton x vx).
 Proof.
  unfold singleton. ok.
 Qed.
 
-(** ** makeBlack, MakeRed *)
+(** *** makeBlack and makeRed *)
 
- #[export] Instance makeBlack_ok m `{!Ok m} : Ok (makeBlack m).
+#[export] Instance makeBlack_ok m `{!Ok m} : Ok (makeBlack m).
 Proof.
  destruct m; simpl; ok.
 Qed.
 
- #[export] Instance makeRed_ok m `{!Ok m} : Ok (makeRed m).
+#[export] Instance makeRed_ok m `{!Ok m} : Ok (makeRed m).
 Proof.
  destruct m; simpl; ok.
 Qed.
@@ -409,7 +408,7 @@ Proof.
  now destruct m.
 Qed.
 
-(** ** Generic handling for red-matching and red-red-matching *)
+(** *** Generic handling for red-matching and red-red-matching *)
 
 Definition isblack m :=
  match m with Bk _ _ _ _ => True | _ => False end.
@@ -532,7 +531,7 @@ Proof.
  exact (rmatch _ _ _).
 Qed.
 
-(** ** Balancing for insertion *)
+(** *** Balancing for insertion *)
 
  #[export] Instance lbal_ok l x v r `(!Ok l, !Ok r, l < x, x < r) :
  Ok (lbal l x v r).
@@ -617,7 +616,7 @@ Qed.
 Hint Rewrite (@in_node elt) makeRed_in makeBlack_in : map.
 Hint Rewrite lbal_in rbal_in rbal'_in : map.
 
-(** ** Insertion *)
+(** *** Insertion *)
 
 Lemma ins_in m x v y :
  y ∈ (ins x v m) <-> y == x \/ y ∈ m.
@@ -638,7 +637,7 @@ Proof.
 Qed.
 Local Hint Resolve ins_above ins_below : map.
 
- #[export] Instance ins_ok m x v `{!Ok m} : Ok (ins x v m).
+#[export] Instance ins_ok m x v `{!Ok m} : Ok (ins x v m).
 Proof.
  induct m; auto; destmatch;
  (eapply lbal_ok || eapply rbal_ok || ok); auto; treeorder.
@@ -670,7 +669,7 @@ Proof.
  - apply ins_spec2; trivial; order.
 Qed.
 
- #[export] Instance add_ok m x v `{!Ok m} : Ok (add x v m).
+#[export] Instance add_ok m x v `{!Ok m} : Ok (add x v m).
 Proof.
  unfold add; autok.
 Qed.
@@ -693,10 +692,9 @@ Proof.
 unfold add. rewrite makeBlack_find. now apply ins_spec2.
 Qed.
 
+(** *** Balancing for deletion *)
 
-(** ** Balancing for deletion *)
-
- #[export] Instance lbalS_ok l x v r :
+#[export] Instance lbalS_ok l x v r :
   forall `(!Ok l, !Ok r, l < x, x < r), Ok (lbalS l x v r).
 Proof.
  case lbalS_match; intros; destmatch; try treeorder; invok; invlt.
@@ -766,7 +764,7 @@ Qed.
 
 Hint Rewrite lbalS_in rbalS_in : map.
 
-(** ** Append for deletion *)
+(** *** Append for deletion *)
 
 Ltac append_tac l r :=
  induction l as [| lc ll _ lx lv lr IHlr];
@@ -820,7 +818,7 @@ Qed.
 
 Hint Rewrite append_in : map.
 
- #[export] Instance append_ok : forall l r `{!Ok l, !Ok r},
+#[export] Instance append_ok : forall l r `{!Ok l, !Ok r},
  l < r -> Ok (@append elt l r).
 Proof.
  append_tac l r; trivial; intros OK OK' AP;
@@ -838,7 +836,7 @@ Proof.
    simpl. destmatch; try apply lbalS_ok; invlt; ok; intuition; eautom.
 Qed.
 
-(** ** Deletion *)
+(** *** Deletion *)
 
 Lemma del_in m x y `{!Ok m} :
  y ∈ (del x m) <-> y ∈ m /\ ~ y==x.
@@ -893,7 +891,7 @@ Qed.
 
 Hint Rewrite remove_in : map.
 
- #[export] Instance remove_ok m x `{!Ok m} : Ok (remove x m).
+#[export] Instance remove_ok m x `{!Ok m} : Ok (remove x m).
 Proof.
 unfold remove; ok.
 Qed.
@@ -909,7 +907,7 @@ Proof.
 unfold remove. rewrite makeBlack_find. now apply del_spec2.
 Qed.
 
-(** ** Treeify *)
+(** *** Treeify *)
 
 Local Notation ifpred p n := (if p then pred n else n%nat).
 Local Notation treeify_t := (klist elt -> t elt * klist elt).
@@ -1578,7 +1576,7 @@ Qed.
 
 End Merge.
 
-(** ** Filtering *)
+(** *** Filtering *)
 
 Section Filter.
 Variable elt : Type.
@@ -1608,7 +1606,7 @@ Definition partition f m :=
   let (l1,l2) := partition_aux f m nil nil in
   (treeify l1, treeify l2).
 
-(** ** Filter *)
+(** *** Filter *)
 
 Lemma filter_aux_bindings f m acc :
  filter_aux f m acc = List.filter (fun '(k,e) => f k e) (bindings m) ++ acc.
@@ -1651,7 +1649,7 @@ Proof.
 Qed.
 
 
-(** ** Partition *)
+(** *** Partition *)
 
 Lemma partition_aux_spec f m acc1 acc2 :
  partition_aux f m acc1 acc2 =
@@ -1698,7 +1696,7 @@ Qed.
 End Filter.
 End MakeRaw.
 
-(** * Encapsulation
+(** ** Encapsulation
 
    Now, in order to really provide a functor implementing [S], we
    need to encapsulate everything into a type of binary search trees. *)
diff --git a/theories/RBTproofs.v b/theories/RBTproofs.v
index 99fbd80..9f43a32 100644
--- a/theories/RBTproofs.v
+++ b/theories/RBTproofs.v
@@ -1,5 +1,8 @@
+(** * Finite Modular Maps: RBT Proofs *)
 
-(** * Finite Modular Maps : RBT Proofs *)
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
+    adapted from earlier works in Coq Standard Library, see README.md.
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This is a complement to [MMaps.RBT], proving the Red/Black balancing
     invariants for the code in [MMaps.RBT], and hence the logarithmic
@@ -30,7 +33,7 @@ Local Arguments Leaf {elt}.
 Local Notation Rd := (@Node _ Red).
 Local Notation Bk := (@Node _ Black).
 
-(** ** Red-Black invariants *)
+(** ** Red-black invariants *)
 
 (** In a red-black tree :
     - a red node has no red children
@@ -65,7 +68,7 @@ Inductive arbt elt (n:nat)(t:tree elt) : Prop :=
 
 Class Rbt elt (t:tree elt) :=  RBT : exists d, rbt d t.
 
-(** ** Basic tactics and results about red-black *)
+(** ** Basic tactics and results about red-black trees *)
 
 Scheme rbt_ind := Induction for rbt Sort Prop.
 Local Hint Constructors rbt rrt arbt : map.
@@ -106,7 +109,7 @@ Qed.
 
 Local Hint Resolve arb_nrr_rb arb_nr_rb : map.
 
-(** ** A Red-Black tree has indeed a logarithmic depth *)
+(** ** A red-black tree has a logarithmic depth *)
 
 Definition redcarac s :=
  rcase (elt:=elt) (fun _ _ _ _ => 1) (fun _ => 0) s.
@@ -168,7 +171,7 @@ Proof.
  unfold singleton. exists 1; autom.
 Qed.
 
-(** ** [makeBlack] and [makeRed] *)
+(** ** makeBlack and makeRed *)
 
 Lemma makeBlack_rb n t : arbt n t -> Rbt (makeBlack t).
 Proof.
diff --git a/theories/Raw.v b/theories/Raw.v
index 63772e2..9514894 100644
--- a/theories/Raw.v
+++ b/theories/Raw.v
@@ -1,9 +1,8 @@
+(** * Finite Modular Maps: Raw Interface *)
 
-(** * Finite Modular Maps : Raw Interface *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This "raw" interface isn't meant for general use, see rather the
     [Interface] file for that. The "raw" version has two interests :
@@ -36,6 +35,7 @@
     extra explanations. *)
 
 From MMaps Require Export Comparisons Interface.
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 (* No induction principles for the records below *)
@@ -185,7 +185,7 @@ Module Type WS (K : DecidableType).
   End Specs.
 End WS.
 
-(** ** Raw Maps on ordered keys. *)
+(** ** Raw maps on ordered keys *)
 
 Module Type S (K : OrderedType).
   Include WS K.
diff --git a/theories/Utils.v b/theories/Utils.v
index 4c03edd..0d9602b 100644
--- a/theories/Utils.v
+++ b/theories/Utils.v
@@ -1,10 +1,13 @@
+(** * Finite Modular Maps: bool and list utilities *)
+
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
+    License: LGPL-2.1-only, see file LICENSE. *)
+
 From Coq Require Import List SetoidList.
 Import ListNotations.
 
 Set Implicit Arguments.
 
-(** * Some complements on bool and lists *)
-
 Lemma eq_bool_alt b b' : b=b' <-> (b=true <-> b'=true).
 Proof.
  destruct b, b'; intuition.
diff --git a/theories/WeakList.v b/theories/WeakList.v
index c9d2341..adf4fa7 100644
--- a/theories/WeakList.v
+++ b/theories/WeakList.v
@@ -1,9 +1,8 @@
+(** * Finite Modular Maps: Unordered Lists *)
 
-(** * Finite Modular Maps : Unordered Lists *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 (** This file proposes an implementation of the interface
  [MMaps.Interface.WS] using lists of pairs, unordered but without
@@ -55,7 +54,7 @@ Section Elt.
 
 Variable elt : Type.
 
-(** * [find] *)
+(** ** find *)
 
 Fixpoint find (k:key) (s: t elt) : option elt :=
   match s with
@@ -77,7 +76,7 @@ Proof.
    + rewrite IH; intuition.
 Qed.
 
-(** * [mem] *)
+(** ** mem *)
 
 Fixpoint mem (k : key) (s : t elt) : bool :=
   match s with
@@ -114,7 +113,7 @@ Qed.
 Lemma isok_Ok (m:t elt) : isok m = true -> Ok m.
 Proof. apply isok_spec. Qed.
 
-(** * [empty] *)
+(** ** empty *)
 
 Definition empty : t elt := nil.
 
@@ -123,12 +122,12 @@ Proof.
  reflexivity.
 Qed.
 
- #[export] Instance empty_ok : Ok empty.
+#[export] Instance empty_ok : Ok empty.
 Proof.
  unfold empty; red; auto.
 Qed.
 
-(** * [is_empty] *)
+(** ** is_empty *)
 
 Definition is_empty (l : t elt) : bool := if l then true else false.
 
@@ -152,7 +151,7 @@ Proof.
  elim E. now transitivity x'.
 Qed.
 
-(** * [add] *)
+(** ** add *)
 
 Fixpoint add (k : key) (x : elt) (s : t elt) : t elt :=
   match s with
@@ -191,7 +190,7 @@ Proof.
    + intuition. right; eapply IH; eauto.
 Qed.
 
- #[export] Instance add_ok m x e (Hm:Ok m) : Ok (add x e m).
+#[export] Instance add_ok m x e (Hm:Ok m) : Ok (add x e m).
 Proof.
  induction m as [ | (k,e') m IH]; simpl.
  - constructor; auto. now inversion 1.
@@ -200,7 +199,7 @@ Proof.
    + contradict H; apply add_InA with x e; auto.
 Qed.
 
-(** * [remove] *)
+(** ** remove *)
 
 Fixpoint remove (k : key) (s : t elt) : t elt :=
   match s with
@@ -236,7 +235,7 @@ Proof.
  right; eapply H; eauto.
 Qed.
 
- #[export] Instance remove_ok m x (Hm:Ok m) : Ok (remove x m).
+#[export] Instance remove_ok m x (Hm:Ok m) : Ok (remove x m).
 Proof.
  induction m.
  simpl; intuition.
@@ -248,7 +247,7 @@ Proof.
  contradict H; apply remove_InA with x; auto.
 Qed.
 
-(** * [bindings] *)
+(** ** bindings *)
 
 Definition bindings (m : t elt) := m.
 
@@ -262,7 +261,7 @@ Proof.
  trivial.
 Qed.
 
-(** * [fold] *)
+(** ** fold *)
 
 Fixpoint fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc : A) :  A :=
   match m with
@@ -276,19 +275,19 @@ Proof.
  induction m as [ | (k,e) m IH]; simpl; auto.
 Qed.
 
-(** * [singleton] *)
+(** ** singleton *)
 
 Definition singleton k (e:elt) : t elt := (k,e)::nil.
 
 Lemma singleton_spec x e : bindings (singleton x e) = (x,e)::nil.
 Proof. reflexivity. Qed.
 
- #[export] Instance singleton_ok x e : Ok (singleton x e).
+#[export] Instance singleton_ok x e : Ok (singleton x e).
 Proof.
  constructor; auto. inversion 1.
 Qed.
 
-(** * [equal] *)
+(** ** equal *)
 
 Definition check (cmp : elt -> elt -> bool)(k:key)(e:elt)(m': t elt) :=
   match find k m' with
@@ -394,7 +393,7 @@ End Elt.
 Section Elt2.
 Variable elt elt' : Type.
 
-(** * [map] and [mapi] *)
+(** ** map and mapi *)
 
 Definition map (f:elt -> elt') (m:t elt) : t elt' :=
   List.map (fun '(k,e) => (k,f e)) m.
@@ -417,7 +416,7 @@ Proof.
   intuition.
 Qed.
 
- #[export] Instance map_ok (f:elt->elt') m (Hm : Ok m) : Ok (map f m).
+#[export] Instance map_ok (f:elt->elt') m (Hm : Ok m) : Ok (map f m).
 Proof.
  induction m as [|(x,e) m IH]; simpl. red; constructor.
  inversion_clear Hm. constructor; autok. now rewrite map_InA.
@@ -431,7 +430,7 @@ Proof.
  reflexivity.
 Qed.
 
- #[export] Instance mapi_ok (f: key->elt->elt') m (Hm:Ok m) : Ok (mapi f m).
+#[export] Instance mapi_ok (f: key->elt->elt') m (Hm:Ok m) : Ok (mapi f m).
 Proof.
  induction m as [|(x,e) m IH]; simpl. red; constructor.
  inversion_clear Hm; auto.
@@ -559,7 +558,7 @@ Variable f : key -> option elt -> option elt' -> option elt''.
 Definition merge m m' : t elt'' :=
  fold_keys (fun k => f k (find k m) (find k m')) (domains m m').
 
- #[export] Instance merge_ok m m' (Hm:Ok m)(Hm':Ok m') : Ok (merge m m').
+#[export] Instance merge_ok m m' (Hm:Ok m)(Hm':Ok m') : Ok (merge m m').
 Proof.
  now apply fold_keys_ok, domains_ok.
 Qed.
diff --git a/theories/demo.v b/theories/demo.v
index 28978cb..542d38a 100644
--- a/theories/demo.v
+++ b/theories/demo.v
@@ -1,9 +1,8 @@
+(** * Finite Modular Maps: The Demo *)
 
-(** MMaps Library : the demo *)
-
-(** Author : Pierre Letouzey (Université de Paris - INRIA),
+(** Author: Pierre Letouzey (Université de Paris - INRIA),
     adapted from earlier works in Coq Standard Library, see README.md.
-    Licence : LGPL 2.1, see file LICENSE. *)
+    License: LGPL-2.1-only, see file LICENSE. *)
 
 From Coq Require Import ZArith String Orders List.
 From MMaps Require Import MMaps.
@@ -109,7 +108,7 @@ Compute R.isok raw1.
 Check (eq_refl : R.isok raw1 = true).
 Check (@ZM.Mkt_bool _ raw1 eq_refl).
 
-(** * Some more intense tests. *)
+(** ** Some more intense tests *)
 
 Fixpoint multiples (m:Z)(start:Z)(n:nat) {struct n} : list Z :=
   match n with
@@ -135,7 +134,7 @@ Definition bigmap4 :=
 Time Compute ZM.bindings (ZM.merge both bigmap3 bigmap4).
 
 
-(** * the Facts *)
+(** ** The Facts *)
 
 (* The properties provided by ZM are deliberately minimalistic.
    They correspond to the minimal specifications present in Interface.S.
@@ -164,7 +163,7 @@ Check ZMF.fold_add.
  and for instance RBT.Make_ord *)
 
 
-(** * The Weak Maps *)
+(** ** The Weak Maps *)
 
 (* Sometimes, one may need finite sets and maps over a base type
    that does not come with a decidable order. As long as this type

From 0089e5a91db6cbe7218eeb49bba841db9a712099 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sun, 30 Oct 2022 08:29:52 +0100
Subject: [PATCH 6/6] add coqdoc boilerplate, including deployment

---
 .github/workflows/deploy-coqdoc.yml |  54 +++++++
 .gitignore                          |   2 +
 Makefile.coq.local                  |  20 +++
 resources/config.js                 |  79 +++++++++
 resources/coqdoc.css                | 197 +++++++++++++++++++++++
 resources/coqdocjs.css              | 239 ++++++++++++++++++++++++++++
 resources/coqdocjs.js               | 197 +++++++++++++++++++++++
 resources/footer.html               |   8 +
 resources/header.html               |  27 ++++
 resources/index.html                |  53 ++++++
 resources/index.md                  |  50 ++++++
 11 files changed, 926 insertions(+)
 create mode 100644 .github/workflows/deploy-coqdoc.yml
 create mode 100644 Makefile.coq.local
 create mode 100644 resources/config.js
 create mode 100644 resources/coqdoc.css
 create mode 100644 resources/coqdocjs.css
 create mode 100644 resources/coqdocjs.js
 create mode 100644 resources/footer.html
 create mode 100644 resources/header.html
 create mode 100644 resources/index.html
 create mode 100644 resources/index.md

diff --git a/.github/workflows/deploy-coqdoc.yml b/.github/workflows/deploy-coqdoc.yml
new file mode 100644
index 0000000..ea3f221
--- /dev/null
+++ b/.github/workflows/deploy-coqdoc.yml
@@ -0,0 +1,54 @@
+name: Build and Deploy coqdoc
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build-coqdoc:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Set up Git repository
+        uses: actions/checkout@v2
+
+      - name: Build coqdoc
+        uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: 'coqorg/coq:dev'
+          custom_script: |
+            {{before_install}}
+            startGroup "Build mmaps dependencies"
+              opam pin add -n -y -k path coq-mmaps .
+              opam update -y
+              opam install -y -j "$(nproc)" coq-mmaps --deps-only
+            endGroup
+            startGroup "Add permissions"
+              sudo chown -R coq:coq .
+            endGroup
+            startGroup "Build coqdoc"
+              make -j "$(nproc)"
+              make coqdoc
+            endGroup
+
+      - name: Revert Coq user permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+
+      - name: Copy HTML and CSS and JavaScript
+        run: |
+          mkdir public
+          cp -r resources/index.html docs/ public/
+
+      - name: Deploy to GitHub pages
+        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
+        uses: crazy-max/ghaction-github-pages@v2
+        with:
+          build_dir: public
+          jekyll: false
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.gitignore b/.gitignore
index 2946e04..a322e7b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,3 +8,5 @@
 .Makefile.coq.d
 Makefile.coq
 Makefile.coq.conf
+_build/
+docs/
diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 0000000..7c1528b
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,20 @@
+GLOBFILES = $(VFILES:.v=.glob)
+CSSFILES = resources/coqdoc.css resources/coqdocjs.css
+JSFILES = resources/config.js resources/coqdocjs.js
+HTMLFILES = resources/header.html resources/footer.html
+COQDOCDIR = docs/coqdoc
+
+COQDOCHTMLFLAGS = --toc --toc-depth 3 --index indexpage --html --utf8 -s \
+  --interpolate --no-lib-name --parse-comments \
+  --with-header resources/header.html --with-footer resources/footer.html
+
+coqdoc: $(GLOBFILES) $(VFILES) $(CSSFILES) $(JSFILES) $(HTMLFILES)
+	$(SHOW)'COQDOC -d $(COQDOCDIR)'
+	$(HIDE)mkdir -p $(COQDOCDIR)
+	$(HIDE)$(COQDOC) $(COQDOCHTMLFLAGS) $(COQDOCLIBS) -d $(COQDOCDIR) $(VFILES)
+	$(SHOW)'COPY resources'
+	$(HIDE)cp $(CSSFILES) $(JSFILES) $(COQDOCDIR)
+.PHONY: coqdoc
+
+resources/index.html: resources/index.md
+	pandoc -s -o $@ $<
diff --git a/resources/config.js b/resources/config.js
new file mode 100644
index 0000000..1902b36
--- /dev/null
+++ b/resources/config.js
@@ -0,0 +1,79 @@
+var coqdocjs = coqdocjs || {};
+
+coqdocjs.repl = {
+    "forall": "∀",
+    "exists": "∃",
+    "~": "¬",
+    "/\\": "∧",
+    "\\/": "∨",
+    "->": "→",
+    "<-": "←",
+    "<->": "↔",
+    "=>": "⇒",
+    "<>": "≠",
+    "<=": "≤",
+    ">=": "≥",
+    "el": "∈",
+    "nel": "∉",
+    "<<=": "⊆",
+    "|-": "⊢",
+    ">>": "»",
+    "<<": "⊆",
+    "++": "⧺",
+    "===": "≡",
+    "=/=": "≢",
+    "=~=": "≅",
+    "==>": "⟹",
+    "<==": "⟸",
+    "False": "⊥",
+    "True": "⊤",
+    ":=": "≔",
+    "-|": "⊣",
+    "*": "×",
+    "::": "∷",
+    "lhd": "⊲",
+    "rhd": "⊳",
+    "nat": "ℕ",
+    "alpha": "α",
+    "beta": "β",
+    "gamma": "γ",
+    "delta": "δ",
+    "epsilon": "ε",
+    "eta": "η",
+    "iota": "ι",
+    "kappa": "κ",
+    "lambda": "λ",
+    "mu": "μ",
+    "nu": "ν",
+    "omega": "ω",
+    "phi": "ϕ",
+    "pi": "π",
+    "psi": "ψ",
+    "rho": "ρ",
+    "sigma": "σ",
+    "tau": "τ",
+    "theta": "θ",
+    "xi": "ξ",
+    "zeta": "ζ",
+    "Delta": "Δ",
+    "Gamma": "Γ",
+    "Pi": "Π",
+    "Sigma": "Σ",
+    "Omega": "Ω",
+    "Xi": "Ξ"
+};
+
+coqdocjs.subscr = {
+  "0" : "₀",
+  "1" : "₁",
+  "2" : "₂",
+  "3" : "₃",
+  "4" : "₄",
+  "5" : "₅",
+  "6" : "₆",
+  "7" : "₇",
+  "8" : "₈",
+  "9" : "₉",
+};
+
+coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];
diff --git a/resources/coqdoc.css b/resources/coqdoc.css
new file mode 100644
index 0000000..18dad89
--- /dev/null
+++ b/resources/coqdoc.css
@@ -0,0 +1,197 @@
+@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700);
+
+body{
+    font-family: 'Open Sans', sans-serif;
+    font-size: 14px;
+    color: #2D2D2D
+}
+
+a {
+    text-decoration: none;
+    border-radius: 3px;
+    padding-left: 3px;
+    padding-right: 3px;
+    margin-left: -3px;
+    margin-right: -3px;
+    color: inherit;
+    font-weight: bold;
+}
+
+#main .code a, #main .inlinecode a, #toc a {
+    font-weight: inherit;
+}
+
+a[href]:hover, [clickable]:hover{
+    background-color: rgba(0,0,0,0.1);
+    cursor: pointer;
+}
+
+h, h1, h2, h3, h4, h5 {
+    line-height: 1;
+    color: black;
+    text-rendering: optimizeLegibility;
+    font-weight: normal;
+    letter-spacing: 0.1em;
+    text-align: left;
+}
+
+div + br {
+  display: none;
+}
+
+div:empty{ display: none;}
+
+#main h1 {
+	font-size: 2em;
+}
+
+#main h2 {
+	font-size: 1.667rem;
+}
+
+#main h3 {
+	font-size: 1.333em;
+}
+
+#main h4, #main h5, #main h6 {
+	font-size: 1em;
+}
+
+#toc h2 {
+    padding-bottom: 0;
+}
+
+#main .doc {
+    margin: 0;
+    text-align: justify;
+}
+
+.inlinecode, .code, #main pre {
+    font-family: monospace;
+}
+
+.code > br:first-child {
+  display: none;
+}
+
+.doc + .code{
+  margin-top:0.5em;
+}
+
+.block{
+    display: block;
+    margin-top: 5px;
+    margin-bottom: 5px;
+    padding: 10px;
+    text-align: center;
+}
+
+.block img{
+    margin: 15px;
+}
+
+table.infrule {
+  border: 0px;
+  margin-left: 50px;
+  margin-top: 10px;
+  margin-bottom: 10px;
+}
+
+td.infrule {
+    font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace;
+    text-align: center;
+    padding: 0;
+    line-height: 1;
+}
+
+tr.infrulemiddle hr {
+    margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+    color: rgb(60%,60%,60%);
+    padding-left: 1em;
+    padding-bottom: 0.1em
+}
+
+.id[type="constructor"], .id[type="projection"], .id[type="method"],
+.id[title="constructor"], .id[title="projection"], .id[title="method"]  {
+    color: #A30E16;
+}
+
+.id[type="var"], .id[type="variable"],
+.id[title="var"], .id[title="variable"] {
+    color: inherit;
+}
+
+.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"],
+.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] {
+    color: #A6650F;
+}
+
+.id[type="lemma"],
+.id[title="lemma"]{
+    color: #188B0C;
+}
+
+.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"],
+.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{
+ color : #2874AE;
+}
+
+.comment {
+  color: #808080;
+}
+
+/* TOC */
+
+#toc h2{
+  letter-spacing: 0;
+  font-size: 1.333em;
+}
+
+/* Index */
+
+#index {
+    margin: 0;
+    padding: 0;
+    width: 100%;
+}
+
+#index #frontispiece {
+    margin: 1em auto;
+    padding: 1em;
+    width: 60%;
+}
+
+.booktitle { font-size : 140%  }
+.authors { font-size : 90%;
+	         line-height: 115%;  }
+.moreauthors { font-size : 60%  }
+
+#index #entrance {
+    text-align: center;
+}
+
+#index #entrance .spacer {
+    margin: 0 30px 0 30px;
+}
+
+ul.doclist {
+    margin-top: 0em;
+    margin-bottom: 0em;
+}
+
+#toc > * {
+    clear: both;
+}
+
+#toc > a {
+    display: block;
+    float: left;
+    margin-top: 1em;
+}
+
+#toc a h2{
+    display: inline;
+}
diff --git a/resources/coqdocjs.css b/resources/coqdocjs.css
new file mode 100644
index 0000000..959b42e
--- /dev/null
+++ b/resources/coqdocjs.css
@@ -0,0 +1,239 @@
+/* replace unicode */
+
+.id[repl] .hidden {
+  font-size: 0;
+}
+
+.id[repl]:before{
+  content: attr(repl);
+}
+
+/* folding proofs */
+
+@keyframes show-proof {
+    0% {
+      max-height: 1.2em;
+      opacity: 1;
+    }
+    99% {
+      max-height: 1000em;
+    }
+    100%{
+    }
+}
+
+@keyframes hide-proof {
+    from {
+      visibility: visible;
+      max-height: 10em;
+      opacity: 1;
+    }
+    to {
+      max-height: 1.2em;
+    }
+}
+
+.proof {
+  cursor: pointer;
+}
+.proof * {
+  cursor: pointer;
+}
+
+.proof {
+  overflow: hidden;
+  position: relative;
+  transition: opacity 1s;
+  display: inline-block;
+}
+
+.proof[show="false"] {
+  max-height: 1.2em;
+  visibility: visible;
+  opacity: 0.3;
+}
+
+.proof[show="false"][animate] {
+  animation-name: hide-proof;
+  animation-duration: 0.25s;
+}
+
+.proof[show="true"] {
+  animation-name: show-proof;
+  animation-duration: 10s;
+}
+
+.proof[show="true"]:before {
+  content: "\25BC"; /* arrow down */
+}
+.proof[show="false"]:before {
+  content: "\25B6"; /* arrow right */
+}
+
+.proof[show="false"]:hover {
+  visibility: visible;
+  opacity: 0.5;
+}
+
+#toggle-proofs[proof-status="no-proofs"] {
+  display: none;
+}
+
+#toggle-proofs[proof-status="some-hidden"]:before {
+  content: "Show Proofs";
+}
+
+#toggle-proofs[proof-status="all-shown"]:before {
+  content: "Hide Proofs";
+}
+
+
+/* page layout */
+
+html, body {
+  height: 100%;
+  margin:0;
+  padding:0;
+}
+
+@media only screen { /* no div with internal scrolling to allow printing of whole content */
+    body {
+        display: flex;
+        flex-direction: column 
+    }
+
+    #content {
+        flex: 1;
+        overflow: auto;
+        display: flex;
+        flex-direction: column;
+    }
+}
+
+#content:focus {
+  outline: none; /* prevent glow in OS X */
+}
+
+#main {
+    display: block;
+    padding: 16px;
+    padding-top: 1em;
+    padding-bottom: 2em;
+    margin-left: auto;
+    margin-right: auto;
+    max-width: 60em;
+    flex: 1 0 auto;
+}
+
+.libtitle {
+  display: none;
+}
+
+/* header */
+#header {
+  width:100%;
+  padding: 0;
+  margin: 0;
+  display: flex;
+  align-items: center;
+  background-color: rgb(21,57,105);
+  color: white;
+  font-weight: bold;
+  overflow: hidden;
+}
+
+
+.button {
+  cursor: pointer;
+}
+
+#header * {
+    text-decoration: none;
+    vertical-align: middle;
+    margin-left: 15px;
+    margin-right: 15px;
+}
+
+#header > .right, #header > .left {
+  display: flex;
+  flex: 1;
+  align-items: center;
+}
+#header > .left {
+  text-align: left;
+}
+#header > .right {
+  flex-direction: row-reverse;
+}
+
+#header a, #header .button {
+    color: white;
+    box-sizing: border-box;
+}
+
+#header a {
+  border-radius: 0;
+  padding: 0.2em;
+}
+
+#header .button {
+  background-color: rgb(63, 103, 156);
+  border-radius: 1em;
+  padding-left: 0.5em;
+  padding-right: 0.5em;
+  margin: 0.2em;
+}
+
+#header a:hover, #header .button:hover {
+    background-color: rgb(181, 213, 255);
+    color: black;
+}
+
+#header h1 { padding: 0;
+             margin: 0;}
+
+/* footer */
+#footer {
+  text-align: center;
+  opacity: 0.5;
+  font-size: 75%;
+}
+
+/* hyperlinks */
+
+@keyframes highlight {
+    50%{
+      background-color: black;
+    }
+}
+
+:target * {
+  animation-name: highlight;
+  animation-duration: 1s;
+}
+
+a[name]:empty {
+  float: right;
+}
+
+/* Proviola */
+
+div.code {
+  width: auto;
+  float: none;
+}
+
+div.goal {
+  position: fixed;
+  left: 75%;
+  width: 25%;
+  top: 3em;
+}
+
+div.doc {
+  clear: both;
+}
+
+span.command:hover {
+  background-color: inherit;
+}
diff --git a/resources/coqdocjs.js b/resources/coqdocjs.js
new file mode 100644
index 0000000..727da8c
--- /dev/null
+++ b/resources/coqdocjs.js
@@ -0,0 +1,197 @@
+var coqdocjs = coqdocjs || {};
+(function(){
+
+function replace(s){
+  var m;
+  if (m = s.match(/^(.+)'/)) {
+    return replace(m[1])+"'";
+  } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) {
+    return replace(m[1])+m[2].replace(/\d/g, function(d){
+      if (coqdocjs.subscr.hasOwnProperty(d)) {
+        return coqdocjs.subscr[d];
+      } else {
+        return d;
+      }
+    });
+  } else if (coqdocjs.repl.hasOwnProperty(s)){
+    return coqdocjs.repl[s]
+  } else {
+    return s;
+  }
+}
+
+function toArray(nl){
+    return Array.prototype.slice.call(nl);
+}
+
+function replInTextNodes() {
+  // Get all the nodes up front.
+  var nodes = Array.from(document.querySelectorAll(".code, .inlinecode"))
+    .flatMap(elem => Array.from(elem.childNodes)
+          .filter(e => e.nodeType == Node.TEXT_NODE)
+    );
+
+  // Create a replacement template node to clone from.
+  var replacementTemplate = document.createElement("span");
+  replacementTemplate.setAttribute("class", "id");
+  replacementTemplate.setAttribute("type", "keyword");
+
+  // Do the replacements.
+  coqdocjs.replInText.forEach(function(toReplace){
+    var replacement = replacementTemplate.cloneNode(true);
+    replacement.appendChild(document.createTextNode(toReplace));
+
+    nodes.forEach(node => {
+      var fragments = node.textContent.split(toReplace);
+      node.textContent = fragments[fragments.length-1];
+      for (var k = 0; k < fragments.length - 1; ++k) {
+        fragments[k] && node.parentNode.insertBefore(document.createTextNode(fragments[k]),node);
+        node.parentNode.insertBefore(replacement.cloneNode(true), node);
+      }
+    });
+  });
+}
+
+function replNodes() {
+  toArray(document.getElementsByClassName("id")).forEach(function(node){
+    if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){
+      var text = node.textContent;
+      var replText = replace(text);
+      if(text != replText) {
+        node.setAttribute("repl", replText);
+        node.setAttribute("title", text);
+        var hidden = document.createElement("span");
+        hidden.setAttribute("class", "hidden");
+        while (node.firstChild) {
+          hidden.appendChild(node.firstChild);
+        }
+        node.appendChild(hidden);
+      }
+    }
+  });
+}
+
+function isVernacStart(l, t){
+  t = t.trim();
+  for(var s of l){
+    if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){
+      return true;
+    }
+  }
+  return false;
+}
+
+function isProofStart(n){
+    return isVernacStart(["Proof"], n.textContent) ||
+        (isVernacStart(["Next"], n.textContent) && isVernacStart(["Obligation"], n.nextSibling.nextSibling.textContent));
+}
+
+function isProofEnd(s){
+  return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s);
+}
+
+function proofStatus(){
+  var proofs = toArray(document.getElementsByClassName("proof"));
+  if(proofs.length) {
+    for(var proof of proofs) {
+      if (proof.getAttribute("show") === "false") {
+          return "some-hidden";
+      }
+    }
+    return "all-shown";
+  }
+  else {
+    return "no-proofs";
+  }
+}
+
+function updateView(){
+  document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus());
+}
+
+function foldProofs() {
+  var hasCommands = true;
+  var nodes = document.getElementsByClassName("command");
+  if(nodes.length == 0) {
+    hasCommands = false;
+    console.log("no command tags found")
+    nodes = document.getElementsByClassName("id");
+  }
+  toArray(nodes).forEach(function(node){
+    if(isProofStart(node)) {
+      var proof = document.createElement("span");
+      proof.setAttribute("class", "proof");
+
+      node.parentNode.insertBefore(proof, node);
+      if(proof.previousSibling.nodeType === Node.TEXT_NODE)
+        proof.appendChild(proof.previousSibling);
+      while(node && !isProofEnd(node.textContent)) {
+        proof.appendChild(node);
+        node = proof.nextSibling;
+      }
+      if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed
+      if (!hasCommands && proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed
+
+      proof.addEventListener("click", function(proof){return function(e){
+        if (e.target.parentNode.tagName.toLowerCase() === "a")
+          return;
+        proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true");
+        proof.setAttribute("animate", "");
+        updateView();
+      };}(proof));
+      proof.setAttribute("show", "false");
+    }
+  });
+}
+
+function toggleProofs(){
+  var someProofsHidden = proofStatus() === "some-hidden";
+  toArray(document.getElementsByClassName("proof")).forEach(function(proof){
+    proof.setAttribute("show", someProofsHidden);
+    proof.setAttribute("animate", "");
+  });
+  updateView();
+}
+
+function repairDom(){
+  // pull whitespace out of command
+  toArray(document.getElementsByClassName("command")).forEach(function(node){
+    while(node.firstChild && node.firstChild.textContent.trim() == ""){
+      console.log("try move");
+      node.parentNode.insertBefore(node.firstChild, node);
+    }
+  });
+  toArray(document.getElementsByClassName("id")).forEach(function(node){
+    node.setAttribute("type", node.getAttribute("title"));
+  });
+  toArray(document.getElementsByClassName("idref")).forEach(function(ref){
+    toArray(ref.childNodes).forEach(function(child){
+      if (["var", "variable"].indexOf(child.getAttribute("type")) > -1)
+        ref.removeAttribute("href");
+    });
+  });
+
+}
+
+function fixTitle(){
+  var url = "/" + window.location.pathname;
+  var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.'));
+  if (basename === "toc") {document.title = "Table of Contents";}
+  else if (basename === "indexpage") {document.title = "Index";}
+  else {document.title = basename;}
+}
+
+function postprocess(){
+  repairDom();
+  replInTextNodes()
+  replNodes();
+  foldProofs();
+  document.getElementById("toggle-proofs").addEventListener("click", toggleProofs);
+  updateView();
+}
+
+fixTitle();
+document.addEventListener('DOMContentLoaded', postprocess);
+
+coqdocjs.toggleProofs = toggleProofs;
+})();
diff --git a/resources/footer.html b/resources/footer.html
new file mode 100644
index 0000000..8084014
--- /dev/null
+++ b/resources/footer.html
@@ -0,0 +1,8 @@
+</div>
+<div id="footer">
+  Generated by <a href="http://coq.inria.fr">coqdoc</a> and improved with <a href="https://github.com/palmskog/coqdocjs">CoqdocJS</a> as adapted for <a href="https://github.com/coq-community">coq-community</a>
+</div>
+</div>
+</body>
+
+</html>
diff --git a/resources/header.html b/resources/header.html
new file mode 100644
index 0000000..d0c872c
--- /dev/null
+++ b/resources/header.html
@@ -0,0 +1,27 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="config.js"></script>
+<script type="text/javascript" src="coqdocjs.js"></script>
+</head>
+
+<body onload="document.getElementById('content').focus()">
+  <div id="header">
+    <span class="left">
+      <span class="modulename"> <script> document.write(document.title) </script> </span>
+    </span>
+
+    <span class="button" id="toggle-proofs"></span>
+
+    <span class="right">
+      <a href="./../..">Project Website</a>
+      <a href="./indexpage.html">Index</a>
+      <a href="./toc.html">Table of Contents</a>
+    </span>
+</div>
+    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">
diff --git a/resources/index.html b/resources/index.html
new file mode 100644
index 0000000..d46cab1
--- /dev/null
+++ b/resources/index.html
@@ -0,0 +1,53 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
+<head>
+  <meta charset="utf-8" />
+  <meta name="generator" content="pandoc" />
+  <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
+  <title>Modular Finite Maps over Ordered Types</title>
+  <style>
+    code{white-space: pre-wrap;}
+    span.smallcaps{font-variant: small-caps;}
+    span.underline{text-decoration: underline;}
+    div.column{display: inline-block; vertical-align: top; width: 50%;}
+    div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
+    ul.task-list{list-style: none;}
+  </style>
+  <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
+  <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
+  <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
+  <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
+  <style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
+</head>
+<body>
+<header id="title-block-header">
+<h1 class="title">Modular Finite Maps over Ordered Types</h1>
+</header>
+<div style="text-align:left">
+<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"> <a href="https://github.com/coq-community/coq-mmaps">View the project on GitHub</a> <img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
+</div>
+<h2 id="about">About</h2>
+<p>Welcome to the Modular Finite Maps over Ordered Types project website! This project is part of <a href="https://github.com/coq-community/manifesto">coq-community</a>.</p>
+<p>This project contains several implementations of finite maps, including implementations based on AVL trees and red-black trees. The finite maps are parameterized on arbitrary ordered types using Coq functors. This is an updated version of the Coq Stdlib’s FMaps that is meant to complement the Stdlib’s MSet library.</p>
+<p>This is an open source project, licensed under the GNU Lesser General Public License v2.1 only.</p>
+<h2 id="get-the-code">Get the code</h2>
+<p>The current stable release of Modular Finite Maps over Ordered Types can be <a href="https://github.com/coq-community/coq-mmaps/releases">downloaded from GitHub</a>.</p>
+<h2 id="documentation">Documentation</h2>
+<p>See the <a href="https://coq-community.org/coq-mmaps/docs/coqdoc/toc.html">latest coqdoc documentation</a>.</p>
+<p>Related publications:</p>
+<ul>
+<li><a href="https://www.cs.princeton.edu/~appel/papers/redblack.pdf">Efficient Verified Red-Black Trees</a></li>
+<li><a href="https://hal.inria.fr/hal-00150913">Functors for Proofs and Programs</a> doi:<a href="https://doi.org/10.1007/978-3-540-24725-8_26">10.1007/978-3-540-24725-8_26</a></li>
+</ul>
+<h2 id="help-and-contact">Help and contact</h2>
+<ul>
+<li>Report issues on <a href="https://github.com/coq-community/coq-mmaps/issues">GitHub</a></li>
+<li>Chat with us on <a href="https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users">Zulip</a></li>
+<li>Discuss with us on Coq’s <a href="https://coq.discourse.group">Discourse</a> forum</li>
+</ul>
+<h2 id="authors">Authors</h2>
+<ul>
+<li>Pierre Letouzey</li>
+</ul>
+</body>
+</html>
diff --git a/resources/index.md b/resources/index.md
new file mode 100644
index 0000000..6e5a9dc
--- /dev/null
+++ b/resources/index.md
@@ -0,0 +1,50 @@
+---
+title: Modular Finite Maps over Ordered Types
+lang: en
+header-includes:
+  - |
+    <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
+    <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
+    <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
+    <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
+    <style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
+---
+
+<div style="text-align:left"><img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
+<a href="https://github.com/coq-community/coq-mmaps">View the project on GitHub</a>
+<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"></div>
+
+## About
+
+Welcome to the Modular Finite Maps over Ordered Types project website! This project is part of [coq-community](https://github.com/coq-community/manifesto).
+
+This project contains several implementations of finite maps,
+including implementations based on AVL trees and red-black trees.
+The finite maps are parameterized on arbitrary ordered types using
+Coq functors. This is an updated version of the Coq Stdlib's FMaps
+that is meant to complement the Stdlib's MSet library.
+
+This is an open source project, licensed under the GNU Lesser General Public License v2.1 only.
+
+## Get the code
+
+The current stable release of Modular Finite Maps over Ordered Types can be [downloaded from GitHub](https://github.com/coq-community/coq-mmaps/releases).
+
+## Documentation
+
+See the [latest coqdoc documentation](https://coq-community.org/coq-mmaps/docs/coqdoc/toc.html).
+
+Related publications:
+
+- [Efficient Verified Red-Black Trees](https://www.cs.princeton.edu/~appel/papers/redblack.pdf) 
+- [Functors for Proofs and Programs](https://hal.inria.fr/hal-00150913) doi:[10.1007/978-3-540-24725-8_26](https://doi.org/10.1007/978-3-540-24725-8_26)
+
+## Help and contact
+
+- Report issues on [GitHub](https://github.com/coq-community/coq-mmaps/issues)
+- Chat with us on [Zulip](https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users)
+- Discuss with us on Coq's [Discourse](https://coq.discourse.group) forum
+
+## Authors
+
+- Pierre Letouzey