coqdoc: fix syntax

Author: liyishuai

Makefile

@@ -30,7 +30,7 @@ dist:
 
 TEMPLATES ?= ../templates
 
-docs/index.html: index.md
+index.html: index.md
 	pandoc -s $^ -o $@
 
 index.md: meta.yml

meta.yml

@@ -65,6 +65,7 @@ documentation: |
     - Base directory to the provided theories
 
 coqdoc_index: |
+  - [0.11.2](v0.11.2/toc.html)
   - [0.11.1](v0.11.1/toc.html)
   - [0.11.0](v0.11.0/toc.html)
   - [0.10.3](v0.10.3/toc.html)

theories/Data/Eq/UIP_trans.v

@@ -1,7 +1,7 @@
 (** The contents in this file are reconstructed from the proof of Bruno Barras
- ** in the Coq standard library. It is duplicated so that the definitions
- ** can be made transparent, and therefore computable.
- ** See Coq.Logic.Eqdep_dec for complete information
+    in the Coq standard library. It is duplicated so that the definitions
+    can be made transparent, and therefore computable.
+    See Coq.Logic.Eqdep_dec for complete information
  **)
 Section uip_trans.
   Context {A : Type}.
@@ -65,4 +65,4 @@ Section uip_trans.
                                  | left pf => or_introl pf
                                  | right pf' => or_intror pf'
                                  end).
-End uip_trans.
+End uip_trans.

theories/Data/Fin.v

@@ -9,7 +9,7 @@ Set Strict Implicit.
 Set Asymmetric Patterns.
 
 (** `fin n` corresponds to "naturals less than `n`",
- ** i.e. a finite set of size n
+    i.e. a finite set of size n
  **)
 Inductive fin : nat -> Type :=
 | F0 : forall {n}, fin (S n)
@@ -112,4 +112,4 @@ Proof.
   eapply H.
   inv_all ; subst.
   apply IHx. reflexivity.
-Qed.
+Qed.

theories/Data/HList.v

@@ -701,7 +701,7 @@ Arguments Hcons {_ _ _ _} _ _.
 Arguments equiv_hlist {_ F} R {_} _ _ : rename.
 
 (** Weak Map
- ** This is weak because it does not change the key type
+    This is weak because it does not change the key type
  **)
 Section hlist_map.
   Variable A : Type.

theories/Data/Lazy.v

@@ -8,7 +8,7 @@ Set Strict Implicit.
 Definition Lazy (t : Type) : Type := unit -> t.
 
 (** Note: in order for this to have the right behavior, it must
- ** be beta-delta reduced.
+    be beta-delta reduced.
  **)
 Definition _lazy {T : Type} (l : T) : Lazy T := fun _ => l.
 

theories/Data/Monads/FuelMonad.v

@@ -12,7 +12,7 @@ Arguments Diverge {_}.
 Arguments Term {_} _.
 
 (** The GFix monad is like monad fix except that
- ** it encapsulates the "gas" that is used as the measure
+    it encapsulates the "gas" that is used as the measure
  **)
 Section gfix.
   (** This is essentially ReaderT (optionT m)) **)

theories/Data/Monads/WriterMonad.v

@@ -128,7 +128,7 @@ End CastWriterT.
 
 
 (** Simple wrapper around `writerT` specializing the underlying monad to `Identity`
- ** which yields the `writer` monad.
+    which yields the `writer` monad.
  **)
 Section WriterMonad.
 

theories/Data/Set/SetMap.v

@@ -5,7 +5,7 @@ Set Implicit Arguments.
 Set Strict Implicit.
 
 (** Canonical instance, a set is the same as a map where the values
- ** are unit
+    are unit
  **)
 (*
 Section SetFromMap.
@@ -26,4 +26,4 @@ Section SetFromMap.
   ; singleton := fun v => Maps.add v tt Maps.empty
   }.
 End SetFromMap.
-*)
+*)

theories/Structures/MonadLaws.v

@@ -12,11 +12,11 @@ Section MonadLaws.
   Variable M : Monad m.
 
   (** This <= relation is a computational <= relation based on the ideas
-   ** of domain theory. It generalizes the usual equivalence relation by,
-   ** enabling the relation to talk about computations that are "more defined"
-   ** than others.
-   **
-   ** This generalization is done to support the fixpoint law.
+      of domain theory. It generalizes the usual equivalence relation by,
+      enabling the relation to talk about computations that are "more defined"
+      than others.
+   
+      This generalization is done to support the fixpoint law.
    **)
 
   Class MonadLaws :=