Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.

182 files changed, 751 insertions, 626 deletions

diff --git a/.merlin.in b/.merlin.in
index 4d646842d8..fa3473765d 100644
--- a/.merlin.in
+++ b/.merlin.in
@@ -1,4 +1,4 @@
-FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50
+FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48
 
 S clib
 B clib
diff --git a/checker/analyze.ml b/checker/analyze.ml
index 7047d8a149..63324bff20 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -396,7 +396,7 @@ let parse_string s = PString.parse (s, ref 0)
 let instantiate (p, mem) =
   let len = LargeArray.length mem in
   let ans = LargeArray.make len (Obj.repr 0) in
-  (** First pass: initialize the subobjects *)
+  (* First pass: initialize the subobjects *)
   for i = 0 to len - 1 do
     let obj = match LargeArray.get mem i with
     | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
@@ -408,9 +408,9 @@ let instantiate (p, mem) =
   | Int n -> Obj.repr n
   | Ptr p -> LargeArray.get ans p
   | Atm tag -> Obj.new_block tag 0
-  | Fun _ -> assert false (** We shouldn't serialize closures *)
+  | Fun _ -> assert false (* We shouldn't serialize closures *)
   in
-  (** Second pass: set the pointers *)
+  (* Second pass: set the pointers *)
   for i = 0 to len - 1 do
     match LargeArray.get mem i with
     | Struct (_, blk) ->
diff --git a/checker/analyze.mli b/checker/analyze.mli
index 9c837643fa..d7770539df 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -30,6 +30,7 @@ sig
   type t
   val input_byte : t -> int
   (** Input a single byte *)
+
   val input_binary_int : t -> int
   (** Input a big-endian 31-bits signed integer *)
 end
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 4e026d6f60..ef10bf827d 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -95,11 +95,11 @@ let typecheck_arity env params inds =
 (* Check that the subtyping information inferred for inductive types in the block is correct. *)
 (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
 let check_subtyping cumi paramsctxt env arities =
-    let numparams = Context.Rel.nhyps paramsctxt in
-  (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
-      We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
-      and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
-      with the cumulativity constraints [ cumul_cst ]. *)
+  let numparams = Context.Rel.nhyps paramsctxt in
+  (* In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
+     We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
+     and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
+     with the cumulativity constraints [ cumul_cst ]. *)
   let uctx = ACumulativityInfo.univ_context cumi in
   let len = AUContext.size uctx in
   let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in
@@ -238,7 +238,7 @@ let check_inductive env kn mib =
       let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in
       Environ.push_context uctx env
   in
-  (** Locally set the oracle for further typechecking *)
+  (* Locally set the oracle for further typechecking *)
   let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b83fe831bb..086dd17e39 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -10,10 +10,10 @@ open Environ
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  (** Locally set the oracle for further typechecking *)
+  (* Locally set the oracle for further typechecking *)
   let oracle = env.env_typing_flags.conv_oracle in
   let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
-  (** [env'] contains De Bruijn universe variables *)
+  (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
     | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
@@ -40,7 +40,7 @@ let check_constant_declaration env kn cb =
     if poly then add_constant kn cb env
     else add_constant kn cb env'
   in
-  (** Reset the value of the oracle *)
+  (* Reset the value of the oracle *)
   Environ.set_oracle env oracle
 
 (** {6 Checking modules } *)
diff --git a/checker/votour.ml b/checker/votour.ml
index 1ea0de456e..3c088b59b5 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -366,7 +366,7 @@ let visit_vo f =
   |] in
   let repr =
     if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S)
-    (** On 32-bit machines, representation may exceed the max size of arrays *)
+    (* On 32-bit machines, representation may exceed the max size of arrays *)
   in
   let module Repr = (val repr : S) in
   let module Visit = Visit(Repr) in
diff --git a/clib/backtrace.ml b/clib/backtrace.ml
index 27ed6fbf72..64faa5fd2e 100644
--- a/clib/backtrace.ml
+++ b/clib/backtrace.ml
@@ -87,8 +87,8 @@ let get_backtrace e =
 
 let add_backtrace e =
   if !is_recording then
-    (** This must be the first function call, otherwise the stack may be
-        destroyed *)
+    (* This must be the first function call, otherwise the stack may be
+       destroyed *)
     let current = get_exception_backtrace () in
     let info = Exninfo.info e in
     begin match current with
diff --git a/clib/bigint.mli b/clib/bigint.mli
index ac66b41fb7..88297c353d 100644
--- a/clib/bigint.mli
+++ b/clib/bigint.mli
@@ -25,6 +25,7 @@ val one : bigint
 val two : bigint
 
 val div2_with_rest : bigint -> bigint * bool (** true=odd; false=even *)
+
 val add_1 : bigint -> bigint
 val sub_1 : bigint -> bigint
 val mult_2 : bigint -> bigint
diff --git a/clib/cArray.ml b/clib/cArray.ml
index c3a693ff16..e0a1859184 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -451,7 +451,7 @@ struct
       end
     done;
     if !i < len then begin
-      (** The array is not the same as the original one *)
+      (* The array is not the same as the original one *)
       let ans : 'a array = Array.copy ar in
       let v = match !temp with None -> assert false | Some x -> x in
       Array.unsafe_set ans !i v;
@@ -483,7 +483,7 @@ struct
       end
     done;
     if !i < len then begin
-      (** The array is not the same as the original one *)
+      (* The array is not the same as the original one *)
       let ans : 'a array = Array.copy ar in
       let v = match !temp with None -> assert false | Some x -> x in
       Array.unsafe_set ans !i v;
@@ -504,7 +504,7 @@ struct
     let i = ref 0 in
     let break = ref true in
     let r = ref accu in
-    (** This variable is never accessed unset *)
+    (* This variable is never accessed unset *)
     let temp = ref None in
     while !break && (!i < len) do
       let v = Array.unsafe_get ar !i in
@@ -539,7 +539,7 @@ struct
     let i = ref 0 in
     let break = ref true in
     let r = ref accu in
-    (** This variable is never accessed unset *)
+    (* This variable is never accessed unset *)
     let temp = ref None in
     while !break && (!i < len) do
       let v = Array.unsafe_get ar !i in
@@ -620,7 +620,7 @@ struct
         end
       done;
       if !i < len then begin
-        (** The array is not the same as the original one *)
+        (* The array is not the same as the original one *)
         let ans : 'a array = Array.copy ar in
         let v = match !temp with None -> assert false | Some x -> x in
         Array.unsafe_set ans !i v;
diff --git a/clib/cString.mli b/clib/cString.mli
index a73c2729d0..364b6a34b1 100644
--- a/clib/cString.mli
+++ b/clib/cString.mli
@@ -31,8 +31,8 @@ sig
   (** [implode [s1; ...; sn]] returns [s1 ^ ... ^ sn] *)
 
   val strip : string -> string
-  (** Alias for [String.trim] *)
   [@@ocaml.deprecated "Use [trim]"]
+  (** Alias for [String.trim] *)
 
   val drop_simple_quotes : string -> string
   (** Remove the eventual first surrounding simple quotes of a string. *)
@@ -53,8 +53,8 @@ sig
   (** Generate the ordinal number in English. *)
 
   val split : char -> string -> string list
-  (** [split c s] alias of [String.split_on_char] *)
   [@@ocaml.deprecated "Use [split_on_char]"]
+  (** [split c s] alias of [String.split_on_char] *)
 
   val is_sub : string -> string -> int -> bool
   (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *)
diff --git a/clib/exninfo.ml b/clib/exninfo.ml
index 2d13049882..78ebd81f7e 100644
--- a/clib/exninfo.ml
+++ b/clib/exninfo.ml
@@ -89,18 +89,18 @@ let find_and_remove () =
 let info e =
   let (src, data) = find_and_remove () in
   if src == e then
-    (** Slightly unsound, some exceptions may not be unique up to pointer
-        equality. Though, it should be quite exceptional to be in a situation
-        where the following holds:
-
-        1. An argument-free exception is raised through the enriched {!raise};
-        2. It is not captured by any enriched with-clause (which would reset
-            the current data);
-        3. The same exception is raised through the standard raise, accessing
-            the wrong data.
+    (* Slightly unsound, some exceptions may not be unique up to pointer
+       equality. Though, it should be quite exceptional to be in a situation
+       where the following holds:
+
+       1. An argument-free exception is raised through the enriched {!raise};
+       2. It is not captured by any enriched with-clause (which would reset
+          the current data);
+       3. The same exception is raised through the standard raise, accessing
+          the wrong data.
     . *)
     data
   else
-    (** Mismatch: the raised exception is not the one stored, either because the
-        previous raise was not instrumented, or because something went wrong. *)
+    (* Mismatch: the raised exception is not the one stored, either because the
+       previous raise was not instrumented, or because something went wrong. *)
     Store.empty
diff --git a/clib/hMap.mli b/clib/hMap.mli
index b26d0e04e3..ab2a6bbf15 100644
--- a/clib/hMap.mli
+++ b/clib/hMap.mli
@@ -13,6 +13,7 @@ sig
   type t
   val compare : t -> t -> int
   (** Total ordering *)
+
   val hash : t -> int
   (** Hashing function compatible with [compare], i.e. [compare x y = 0] implies
       [hash x = hash y]. *)
diff --git a/clib/hashcons.mli b/clib/hashcons.mli
index 223dd2a4d2..e97708cdf3 100644
--- a/clib/hashcons.mli
+++ b/clib/hashcons.mli
@@ -29,17 +29,21 @@ module type HashconsedType =
 
     type t
     (** Type of objects to hashcons. *)
+
     type u
     (** Type of hashcons functions for the sub-structures contained in [t].
         Usually a tuple of functions. *)
+
     val hashcons :  u -> t -> t
     (** The actual hashconsing function, using its fist argument to recursively
         hashcons substructures. It should be compatible with [eq], that is
         [eq x (hashcons f x) = true]. *)
+
     val eq : t -> t -> bool
     (** A comparison function. It is allowed to use physical equality
         on the sub-terms hashconsed by the [hashcons] function, but it should be
         insensible to shallow copy of the compared object. *)
+
     val hash : t -> int
     (** A hash function passed to the underlying hashtable structure. [hash]
         should be compatible with [eq], i.e. if [eq x y = true] then
@@ -50,14 +54,19 @@ module type S =
   sig
     type t
     (** Type of objects to hashcons. *)
+
     type u
     (** Type of hashcons functions for the sub-structures contained in [t]. *)
+
     type table
     (** Type of hashconsing tables *)
+
     val generate : u -> table
     (** This create a hashtable of the hashconsed objects. *)
+
     val hcons : table -> t -> t
     (** Perform the hashconsing of the given object within the table. *)
+
     val stats : table -> Hashset.statistics
     (** Recover statistics of the hashconsing table. *)
   end
diff --git a/clib/hashset.mli b/clib/hashset.mli
index 0699d4e848..6ed93d5fe7 100644
--- a/clib/hashset.mli
+++ b/clib/hashset.mli
@@ -31,18 +31,23 @@ type statistics = {
 module type S = sig
   type elt
   (** Type of hashsets elements. *)
+
   type t
   (** Type of hashsets. *)
+
   val create : int -> t
   (** [create n] creates a fresh hashset with initial size [n]. *)
+
   val clear : t -> unit
   (** Clear the contents of a hashset. *)
+
   val repr : int -> elt -> t -> elt
   (** [repr key constr set] uses [key] to look for [constr]
       in the hashet [set]. If [constr] is in [set], returns the
       specific representation that is stored in [set]. Otherwise,
       [constr] is stored in [set] and will be used as the canonical
       representation of this value in the future. *)
+
   val stats : t -> statistics
   (** Recover statistics on the table. *)
 end
diff --git a/clib/int.ml b/clib/int.ml
index 3ae836aec9..fa21379565 100644
--- a/clib/int.ml
+++ b/clib/int.ml
@@ -114,8 +114,8 @@ struct
           let () = t := DSet (i, old, res) in
           res
       else match v with
-      | None -> t (** Nothing to do! *)
-      | Some _ -> (** we must resize *)
+      | None -> t (* Nothing to do! *)
+      | Some _ -> (* we must resize *)
         let nlen = next len (succ i) in
         let nlen = min nlen Sys.max_array_length in
         let () = assert (i < nlen) in
diff --git a/clib/int.mli b/clib/int.mli
index 76aecf057b..e02ca90916 100644
--- a/clib/int.mli
+++ b/clib/int.mli
@@ -33,10 +33,13 @@ sig
   type 'a t
   (** Persistent, auto-resizable arrays. The [get] and [set] functions never
       fail whenever the index is between [0] and [Sys.max_array_length - 1]. *)
+
   val empty : int -> 'a t
   (** The empty array, with a given starting size. *)
+
   val get : 'a t -> int -> 'a option
   (** Get a value at the given index. Returns [None] if undefined. *)
+
   val set : 'a t -> int -> 'a option -> 'a t
   (** Set/unset a value at the given index. *)
 end
diff --git a/clib/segmenttree.ml b/clib/segmenttree.ml
index 24243b7a99..c3f1b44ef4 100644
--- a/clib/segmenttree.ml
+++ b/clib/segmenttree.ml
@@ -34,16 +34,16 @@ type elt = int
     integers which are _not_ in the set of keys handled by the tree. On 
     leaves, a domain represents the st of integers which are in the set of 
     keys. *)
-type domain = 
-    (** On internal nodes, a domain [Interval (a, b)] represents 
-	the interval [a + 1; b - 1]. On leaves, it represents [a; b]. 
-	We always have [a] <= [b]. *)
+type domain =
   | Interval of elt * elt
-      (** On internal node or root, a domain [Universe] represents all
-	  the integers. When the tree is not a trivial root,
-	  [Universe] has no interpretation on leaves. (The lookup
-	  function should never reach the leaves.) *)
+  (** On internal nodes, a domain [Interval (a, b)] represents
+      the interval [a + 1; b - 1]. On leaves, it represents [a; b].
+      We always have [a] <= [b]. *)
   | Universe
+  (** On internal node or root, a domain [Universe] represents all
+      the integers. When the tree is not a trivial root,
+      [Universe] has no interpretation on leaves. (The lookup
+      function should never reach the leaves.) *)
 
 (** We use an array to store the almost complete tree. This array
     contains at least one element. *)
@@ -71,26 +71,26 @@ let make segments =
   let tree = create nsegments (Universe, None) in 
   let leaves_offset = (1 lsl (log2n nsegments)) - 1 in
 
-    (** The algorithm proceeds in two steps using an intermediate tree
-	to store minimum and maximum of each subtree as annotation of
-	the node. *)
+    (* The algorithm proceeds in two steps using an intermediate tree
+       to store minimum and maximum of each subtree as annotation of
+       the node. *)
 
-    (** We start from leaves: the last level of the tree is initialized
-	with the given segments... *)
-    list_iteri 
+    (* We start from leaves: the last level of the tree is initialized
+       with the given segments... *)
+    list_iteri
       (fun i ((start, stop), value) ->
 	 let k = leaves_offset + i in
 	 let i = Interval (start, stop) in
 	   tree.(k) <- (i, Some i))
       segments;
-    (** ... the remaining leaves are initialized with neutral information. *)
+    (* ... the remaining leaves are initialized with neutral information. *)
     for k = leaves_offset + nsegments to Array.length tree -1 do 
       tree.(k) <- (Universe, Some Universe)
     done;
     
-    (** We traverse the tree bottom-up and compute the interval and
-	annotation associated to each node from the annotations of its
-	children. *)
+    (* We traverse the tree bottom-up and compute the interval and
+       annotation associated to each node from the annotations of its
+       children. *)
     for k = leaves_offset - 1 downto 0 do
       let node, annotation = 
 	match value_of (left_child k) tree, value_of (right_child k) tree with
@@ -104,7 +104,7 @@ let make segments =
 	tree.(k) <- (node, Some annotation)
     done;
 
-    (** Finally, annotation are replaced with the image related to each leaf. *)
+    (* Finally, annotation are replaced with the image related to each leaf. *)
     let final_tree = 
       Array.mapi (fun i (segment, value) -> (segment, None)) tree
     in
diff --git a/clib/trie.ml b/clib/trie.ml
index ea43e9e0bd..96de2b920c 100644
--- a/clib/trie.ml
+++ b/clib/trie.ml
@@ -51,7 +51,7 @@ let next (Node (_,m)) lbl = T_codom.find lbl m
 let get (Node (hereset,_)) = hereset
 
 let labels (Node (_,m)) =
-  (** FIXME: this is order-dependent. Try to find a more robust presentation? *)
+  (* FIXME: this is order-dependent. Try to find a more robust presentation? *)
   List.rev (T_codom.fold (fun x _ acc -> x::acc) m [])
 
 let is_empty_node (Node(a,b)) = (X.is_nil a) && (T_codom.is_empty b)
diff --git a/configure.ml b/configure.ml
index 2559e0a473..33f76078cf 100644
--- a/configure.ml
+++ b/configure.ml
@@ -610,10 +610,9 @@ let camltag = match caml_version_list with
     44: "open" shadowing already defined identifier: too common, especially when some are aliases
     45: "open" shadowing a label or constructor: see 44
     48: implicit elimination of optional arguments: too common
-    50: unexpected documentation comment: too common and annoying to avoid
     58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
 *)
-let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58"
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-58"
 let coq_warn_error =
     if !prefs.warn_error
     then "-warn-error +a"
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 8d728b5b51..cc76c44651 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -26,7 +26,7 @@ let pr_loc loc =
 
 let print_code fmt c =
   let loc = c.loc.loc_start in
-  (** Print the line location as a source annotation *)
+  (* Print the line location as a source annotation *)
   let padding = String.make (loc.pos_cnum - loc.pos_bol + 1) ' ' in
   let code_insert = asprintf "\n# %i \"%s\"\n%s%s" loc.pos_lnum loc.pos_fname padding c.code in
   fprintf fmt "@[@<0>%s@]@\n" code_insert
@@ -471,16 +471,16 @@ let parse_rule self r =
   (symbs, vars, r.tac_body)
 
 let print_rules fmt (name, rules) =
-  (** Rules are reversed. *)
+  (* Rules are reversed. *)
   let rules = List.rev rules in
   let rules = List.map (fun r -> parse_rule name r) rules in
   let pr fmt l = print_list fmt (fun fmt r -> fprintf fmt "(%a)" GramExt.print_extrule r) l in
   match rules with
   | [([SymbEntry (e, None)], [Some s], { code = c } )] when String.trim c = s ->
-    (** This is a horrible hack to work aroud limitations of camlp5 regarding
-        factorization of parsing rules. It allows to recognize rules of the
-        form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and
-        reuse the same entry directly. *)
+    (* This is a horrible hack to work aroud limitations of camlp5 regarding
+       factorization of parsing rules. It allows to recognize rules of the
+       form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and
+       reuse the same entry directly. *)
     fprintf fmt "@[Vernacextend.Arg_alias (%s)@]" e
   | _ -> fprintf fmt "@[Vernacextend.Arg_rules (%a)@]" pr rules
 
diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
new file mode 100644
index 0000000000..f2a113b118
--- /dev/null
+++ b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then
+
+    mtac2_CI_REF=build+warn_50
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b90a53220d..8f207d1e0a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -476,7 +476,7 @@ let pp_generic_argument arg =
 let prgenarginfo arg =
   let Geninterp.Val.Dyn (tag, _) = arg in
   let tpe = Geninterp.Val.pr tag in
-  (** FIXME *)
+  (* FIXME *)
 (*   try *)
 (*     let data = Pptactic.pr_top_generic (Global.env ()) arg in *)
 (*     str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *)
diff --git a/dune b/dune
index aad60d6d46..270738c23c 100644
--- a/dune
+++ b/dune
@@ -1,9 +1,9 @@
 ; Default flags for all Coq libraries.
 (env
- (dev     (flags :standard -rectypes -w -9-27-50+40+60))
+ (dev     (flags :standard -rectypes -w -9-27+40+60))
  (release (flags :standard -rectypes)
           (ocamlopt_flags -O3 -unbox-closures))
- (ireport (flags :standard -rectypes -w -9-27-50+40+60)
+ (ireport (flags :standard -rectypes -w -9-27-40+60)
           (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)))
 
 ; The _ profile could help factoring the above, however it doesn't
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 96f1ce5e60..24d161d00a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -606,6 +606,7 @@ let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
 
 let subst_univs_level_constr subst c =
   of_constr (Vars.subst_univs_level_constr subst (to_constr c))
+
 (** Operations that dot NOT commute with evar-normalization *)
 let noccurn sigma n term =
   let rec occur_rec n c = match kind sigma c with
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 69ee5223c4..db56d0628f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -155,7 +155,7 @@ let is_ground_env = memo is_ground_env
 exception NoHeadEvar
 
 let head_evar sigma c =
-  (** FIXME: this breaks if using evar-insensitive code *)
+  (* FIXME: this breaks if using evar-insensitive code *)
   let c = EConstr.Unsafe.to_constr c in
   let rec hrec c = match kind c with
     | Evar (evk,_)   -> evk
@@ -288,7 +288,7 @@ let empty_csubst = {
 }
 
 let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c =
-  (** Safe because this is a substitution *)
+  (* Safe because this is a substitution *)
   let c = EConstr.Unsafe.to_constr c in
   let rec subst n c = match Constr.kind c with
   | Rel m ->
@@ -318,7 +318,7 @@ let update_var src tgt subst =
   in
   match cur with
   | None ->
-    (** Missing keys stand for identity substitution [src ↦ src] *)
+    (* Missing keys stand for identity substitution [src ↦ src] *)
     let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in
     let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in
     { subst with csubst_var; csubst_rev }
@@ -366,8 +366,8 @@ let push_rel_decl_to_named_context
         about this whole name generation problem. *)
     if Flags.is_program_mode () then next_name_away na avoid
     else
-      (** id_of_name_using_hdchar only depends on the rel context which is empty
-          here *)
+      (* id_of_name_using_hdchar only depends on the rel context which is empty
+         here *)
       next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid
   in
   match extract_if_neq id na with
@@ -540,8 +540,8 @@ let restrict_evar evd evk filter ?src candidates =
   | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
   | _ ->
      let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
-     (** Mark new evar as future goal, removing previous one,
-         circumventing Proofview.advance but making Proof.run_tactic catch these. *)
+     (* Mark new evar as future goal, removing previous one,
+        circumventing Proofview.advance but making Proof.run_tactic catch these. *)
      let future_goals = Evd.save_future_goals evd in
      let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in
      let evd = Evd.restore_future_goals evd future_goals in
@@ -779,7 +779,7 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with
   let r =
     try Id.Map.find id cache.cache
     with Not_found ->
-      (** Dummy value *)
+      (* Dummy value *)
       let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
       let () = cache.cache <- Id.Map.add id r cache.cache in
       r
diff --git a/engine/evd.ml b/engine/evd.ml
index 6345046431..7bc3be87a4 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -89,8 +89,8 @@ struct
     | Some f2 -> normalize (CList.filter_with f1 f2)
 
   let apply_subfilter_array filter subfilter =
-    (** In both cases we statically know that the argument will contain at
-        least one [false] *)
+    (* In both cases we statically know that the argument will contain at
+       least one [false] *)
     match filter with
     | None -> Some (Array.to_list subfilter)
     | Some f ->
@@ -395,7 +395,7 @@ let rename evk id (evtoid, idtoev) =
 let reassign_name_defined evk evk' (evtoid, idtoev as names) =
   let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
   match id with
-  | None -> names (** evk' must not be defined *)
+  | None -> names (* evk' must not be defined *)
   | Some id ->
     (EvMap.add evk' id (EvMap.remove evk evtoid),
     Id.Map.add id evk' (Id.Map.remove id idtoev))
@@ -416,7 +416,7 @@ type evar_flags =
     typeclass_evars : Evar.Set.t }
 
 type evar_map = {
-  (** Existential variables *)
+  (* Existential variables *)
   defn_evars : evar_info EvMap.t;
   undf_evars : evar_info EvMap.t;
   evar_names : EvNames.t;
@@ -520,7 +520,7 @@ let inherit_evar_flags evar_flags evk evk' =
 let remove_evar_flags evk evar_flags =
   { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
     obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
-    (** Restriction information is kept. *)
+    (* Restriction information is kept. *)
     restricted_evars = evar_flags.restricted_evars }
 
 (** New evars *)
@@ -1341,14 +1341,14 @@ module MiniEConstr = struct
         | None -> c
       end
     | App (f, args) when isEvar f ->
-      (** Enforce smart constructor invariant on applications *)
+      (* Enforce smart constructor invariant on applications *)
       let ev = destEvar f in
       begin match safe_evar_value sigma ev with
         | None -> c
         | Some f -> whd_evar sigma (mkApp (f, args))
       end
     | Cast (c0, k, t) when isEvar c0 ->
-      (** Enforce smart constructor invariant on casts. *)
+      (* Enforce smart constructor invariant on casts. *)
       let ev = destEvar c0 in
       begin match safe_evar_value sigma ev with
         | None -> c
diff --git a/engine/evd.mli b/engine/evd.mli
index 0a8d1f3287..7560d68805 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -86,7 +86,7 @@ type evar_body =
 type evar_info = {
   evar_concl : econstr;
   (** Type of the evar. *)
-  evar_hyps : named_context_val; (** TODO econstr? *)
+  evar_hyps : named_context_val; (* TODO econstr? *)
   (** Context of the evar. *)
   evar_body : evar_body;
   (** Optional content of the evar. *)
@@ -546,6 +546,7 @@ val univ_flexible_alg : rigid
 type 'a in_evar_universe_context = 'a * UState.t
 
 val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
+
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 
@@ -567,6 +568,7 @@ val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
 val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
     not a local sort variable declared in [evm] *)
+
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
 
 (* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *)
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index b371884ba4..ac0344148a 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -29,8 +29,8 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
 | Depends l ->
   let f arg = f arg >>= function
   | Uniform x ->
-    (** We dispatch the uniform result on each goal under focus, as we know
-        that the [m] argument was actually dependent. *)
+    (* We dispatch the uniform result on each goal under focus, as we know
+       that the [m] argument was actually dependent. *)
     Proofview.Goal.goals >>= fun goals ->
     let ans = List.map (fun g -> (g,x)) goals in
     Proofview.tclUNIT ans
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 4afa817b27..e0c24f049f 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -28,8 +28,10 @@
     from the IO monad ([Proofview] catches errors in its compatibility
     layer, and when lifting goal-level expressions). *)
 exception Exception of exn
+
 (** This exception is used to signal abortion in [timeout] functions. *)
 exception Timeout
+
 (** This exception is used by the tactics to signal failure by lack of
     successes, rather than some other exceptions (like system
     interrupts). *)
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 545334ce9a..3e57baab26 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -28,8 +28,10 @@
     from the IO monad ([Proofview] catches errors in its compatibility
     layer, and when lifting goal-level expressions). *)
 exception Exception of exn
+
 (** This exception is used to signal abortion in [timeout] functions. *)
 exception Timeout
+
 (** This exception is used by the tactics to signal failure by lack of
     successes, rather than some other exceptions (like system
     interrupts). *)
@@ -51,8 +53,10 @@ module NonLogical : sig
 
   val ref : 'a -> 'a ref t
   (** [Pervasives.(:=)] *)
+
   val (:=) : 'a ref -> 'a -> unit t
   (** [Pervasives.(!)] *)
+
   val (!) : 'a ref -> 'a t
 
   val read_line : string t
@@ -67,6 +71,7 @@ module NonLogical : sig
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
   val raise : ?info:Exninfo.info -> exn -> 'a t
+
   (** [try ... with ...] but restricted to {!Exception}. *)
   val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
   val timeout : int -> 'a t -> 'a t
diff --git a/engine/namegen.ml b/engine/namegen.ml
index a67ff6965b..018eca1ba2 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -358,7 +358,7 @@ let next_name_away_with_default_using_types default na avoid t =
 let next_name_away = next_name_away_with_default default_non_dependent_string
 
 let make_all_name_different env sigma =
-  (** FIXME: this is inefficient, but only used in printing *)
+  (* FIXME: this is inefficient, but only used in printing *)
   let avoid = ref (ids_of_named_context_val (named_context_val env)) in
   let sign = named_context_val env in
   let rels = rel_context env in
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 8a93fad8cc..a5308904f5 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -16,6 +16,7 @@ val make_ident : string -> int option -> Id.t
 val repr_ident : Id.t -> string * int option
 
 val atompart_of_id : Id.t -> string  (** remove trailing digits *)
+
 val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)
 
 val add_suffix : Id.t -> string -> Id.t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 304b2dff84..8c15579bb0 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -660,9 +660,9 @@ let unifiable_delayed g l =
 let free_evars sigma l =
   let cache = Evarutil.create_undefined_evars_cache () in
   let map ev =
-  (** Computes the set of evars appearing in the hypotheses, the conclusion or
-      the body of the evar_info [evi]. Note: since we want to use it on goals,
-      the body is actually supposed to be empty. *)
+  (* Computes the set of evars appearing in the hypotheses, the conclusion or
+     the body of the evar_info [evi]. Note: since we want to use it on goals,
+     the body is actually supposed to be empty. *)
     let evi = Evd.find sigma ev in
     let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
     (ev, fevs)
@@ -672,9 +672,9 @@ let free_evars sigma l =
 let free_evars_with_state sigma l =
   let cache = Evarutil.create_undefined_evars_cache () in
   let map ev =
-  (** Computes the set of evars appearing in the hypotheses, the conclusion or
-      the body of the evar_info [evi]. Note: since we want to use it on goals,
-      the body is actually supposed to be empty. *)
+  (* Computes the set of evars appearing in the hypotheses, the conclusion or
+     the body of the evar_info [evi]. Note: since we want to use it on goals,
+     the body is actually supposed to be empty. *)
     let ev = drop_state ev in
     let evi = Evd.find sigma ev in
     let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
@@ -1157,7 +1157,7 @@ module Goal = struct
     let sigma = step.solution in
     let map goal =
       match cleared_alias sigma goal with
-      | None -> None (** ppedrot: Is this check really necessary? *)
+      | None -> None (* ppedrot: Is this check really necessary? *)
       | Some goal ->
         let gl =
           Env.get >>= fun env ->
diff --git a/engine/proofview.mli b/engine/proofview.mli
index cda4808a23..28e793f0fc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -398,6 +398,7 @@ val tclPROGRESS : 'a tactic -> 'a tactic
 val tclCHECKINTERRUPT : unit tactic
 
 exception Timeout
+
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout if fails with [tclZERO Timeout]. *)
 val tclTIMEOUT : int -> 'a tactic -> 'a tactic
@@ -517,8 +518,8 @@ module Goal : sig
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : (t -> unit tactic) -> unit tactic
 
-  (** Like {!enter}, but assumes exactly one goal under focus, raising *)
-  (** a fatal error otherwise. *)
+  (** Like {!enter}, but assumes exactly one goal under focus, raising
+      a fatal error otherwise. *)
   val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic
 
   (** Recover the list of current goals under focus, without evar-normalization.
@@ -612,8 +613,10 @@ module Notations : sig
 
   (** {!tclBIND} *)
   val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+
   (** {!tclTHEN} *)
   val (<*>) : unit tactic -> 'a tactic -> 'a tactic
+
   (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
   val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 98300764df..137770d8f0 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -197,8 +197,8 @@ let compute_evar_dependency_graph sigma =
 
 let evar_dependency_closure n sigma =
   let open Evd in
-  (** Create the DAG of depth [n] representing the recursive dependencies of
-      undefined evars. *)
+  (* Create the DAG of depth [n] representing the recursive dependencies of
+     undefined evars. *)
   let graph = compute_evar_dependency_graph sigma in
   let rec aux n curr accu =
     if Int.equal n 0 then Evar.Set.union curr accu
@@ -209,9 +209,9 @@ let evar_dependency_closure n sigma =
           Evar.Set.union deps accu
         with Not_found -> accu
       in
-      (** Consider only the newly added evars *)
+      (* Consider only the newly added evars *)
       let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
-      (** Merge the others *)
+      (* Merge the others *)
       let accu = Evar.Set.union curr accu in
       aux (n - 1) ncurr accu
   in
@@ -261,13 +261,13 @@ let print_env_short env sigma =
 let pr_evar_constraints sigma pbs =
   let pr_evconstr (pbty, env, t1, t2) =
     let env =
-      (** We currently allow evar instances to refer to anonymous de
-          Bruijn indices, so we protect the error printing code in this
-          case by giving names to every de Bruijn variable in the
-          rel_context of the conversion problem. MS: we should rather
-          stop depending on anonymous variables, they can be used to
-          indicate independency. Also, this depends on a strategy for
-          naming/renaming. *)
+      (* We currently allow evar instances to refer to anonymous de
+         Bruijn indices, so we protect the error printing code in this
+         case by giving names to every de Bruijn variable in the
+         rel_context of the conversion problem. MS: we should rather
+         stop depending on anonymous variables, they can be used to
+         indicate independency. Also, this depends on a strategy for
+         naming/renaming. *)
       Namegen.make_all_name_different env sigma
     in
     print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++
diff --git a/engine/uState.ml b/engine/uState.ml
index 185283225c..6969d2ba44 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -197,7 +197,7 @@ let process_universe_constraints ctx cstrs =
     | Some l -> Inr l
   in
   let equalize_variables fo l l' r r' local =
-    (** Assumes l = [l',0] and r = [r',0] *)
+    (* Assumes l = [l',0] and r = [r',0] *)
     let () =
       if is_local l' then
         instantiate_variable l' r vars
@@ -235,8 +235,8 @@ let process_universe_constraints ctx cstrs =
           match cst with
           | ULe (l, r) ->
             if UGraph.check_leq univs l r then
-              (** Keep Prop/Set <= var around if var might be instantiated by prop or set
-                  later. *)
+              (* Keep Prop/Set <= var around if var might be instantiated by prop or set
+                 later. *)
               match Univ.Universe.level l, Univ.Universe.level r with
               | Some l, Some r ->
                 Univ.Constraint.add (l, Univ.Le, r) local
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index e20055b133..1619ac3d34 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -32,15 +32,15 @@ let add_list_map u t map =
 let choose_canonical ctx flexible algs s =
   let global = LSet.diff s ctx in
   let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
-    (** If there is a global universe in the set, choose it *)
+    (* If there is a global universe in the set, choose it *)
     if not (LSet.is_empty global) then
       let canon = LSet.choose global in
         canon, (LSet.remove canon global, rigid, flexible)
-    else (** No global in the equivalence class, choose a rigid one *)
+    else (* No global in the equivalence class, choose a rigid one *)
         if not (LSet.is_empty rigid) then
           let canon = LSet.choose rigid in
             canon, (global, LSet.remove canon rigid, flexible)
-        else (** There are only flexible universes in the equivalence
+        else (* There are only flexible universes in the equivalence
                  class, choose a non-algebraic. *)
           let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
             if not (LSet.is_empty nonalgs) then
@@ -94,8 +94,8 @@ let find_inst insts v =
   with Found (f,l) -> (f,l)
 
 let compute_lbound left =
- (** The universe variable was not fixed yet.
-     Compute its level using its lower bound. *)
+ (* The universe variable was not fixed yet.
+    Compute its level using its lower bound. *)
   let sup l lbound =
     match lbound with
     | None -> Some l
@@ -154,9 +154,10 @@ let not_lower lower (d,l) =
           * constraints we must keep it. *)
          compare_constraint_type d d' > 0
        with Not_found ->
-         (** No constraint existing on l *) true) l
+         (* No constraint existing on l *) true) l
 
 exception UpperBoundedAlg
+
 (** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
    constraints to [lbound], adding them to [cstrs].
 
@@ -269,7 +270,7 @@ module UPairSet = Set.Make (UPairs)
 
 let normalize_context_set g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
-  (** Keep the Prop/Set <= i constraints separate for minimization *)
+  (* Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
     Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
   in
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 19705f9d36..7e6ed5e4c0 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -35,8 +35,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 let empty_binders = Id.Map.empty
 
 let name_universe lvl =
-  (** Best-effort naming from the string representation of the level. This is
-      completely hackish and should be solved in upper layers instead. *)
+  (* Best-effort naming from the string representation of the level. This is
+     completely hackish and should be solved in upper layers instead. *)
   Id.of_string_soft (Level.to_string lvl)
 
 let compute_instance_binders inst ubinders =
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index 766e96fdfc..100fbc7271 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -10,6 +10,7 @@ exception Exc of Loc.t * exn
        for an error. This exception must not be raised by [raise] but
        rather by [Ploc.raise] (see below), to prevent the risk of several
        encapsulations of [Ploc.Exc]. *)
+
 val raise : Loc.t -> exn -> 'a
    (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc],
        re-raise it (ignoring the new location [loc]), else raise the
@@ -29,9 +30,11 @@ val sub : Loc.t -> int -> int -> Loc.t
    (** [Ploc.sub loc sh len] is the location [loc] shifted with [sh]
        characters and with length [len]. The previous ending position
        of the location is lost. *)
+
 val after : Loc.t -> int -> int -> Loc.t
    (** [Ploc.after loc sh len] is the location just after loc (starting at
        the end position of [loc]) shifted with [sh] characters and of length
        [len]. *)
+
 val with_comment : Loc.t -> string -> Loc.t
    (** Change the comment part of the given location *)
diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml
index 91695e944e..8420d930d5 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -209,7 +209,8 @@ class ['a] list_selection_box
 	      ()
 
     initializer
-      (** create the functions called when the buttons are clicked *)
+
+      (* create the functions called when the buttons are clicked *)
       let f_add () =
         (* get the files to add with the function provided *)
         let l = add_function () in
@@ -300,8 +301,10 @@ class string_param_box param (tt:GData.tooltips) =
   let _ = we#set_text (param.string_to_string param.string_value) in
 
   object (self)
+
     (** This method returns the main box ready to be packed. *)
     method box = hbox#coerce
+
     (** This method applies the new value of the parameter. *)
     method apply =
       let new_value = param.string_of_string we#text in
@@ -347,9 +350,11 @@ class combo_param_box param (tt:GData.tooltips) =
 	fun () -> wc#entry#text
     in
 object (self)
+
   (** This method returns the main box ready to be packed. *)
   method box = hbox#coerce
-    (** This method applies the new value of the parameter. *)
+
+  (** This method applies the new value of the parameter. *)
   method apply =
     let new_value = get_value () in
       if new_value <> param.combo_value then
@@ -404,8 +409,10 @@ class text_param_box param (tt:GData.tooltips) =
   let _ = dbg "text_param_box: object(self)" in
   object (self)
     val wview = wview
+
     (** This method returns the main box ready to be packed. *)
     method box = wf#coerce
+
     (** This method applies the new value of the parameter. *)
     method apply =
       let v = param.string_of_string (buffer#get_text ()) in
@@ -435,8 +442,10 @@ class bool_param_box param (tt:GData.tooltips) =
   let _ = wchk#misc#set_sensitive param.bool_editable in
 
   object (self)
+
     (** This method returns the check button ready to be packed. *)
     method box = wchk#coerce
+
     (** This method applies the new value of the parameter. *)
     method apply =
       let new_value = wchk#active in
@@ -471,8 +480,10 @@ class modifiers_param_box param =
        tooltips#set_tip wev#coerce ~text: help ~privat: help
   in
   object (self)
+
     (** This method returns the main box ready to be packed. *)
     method box = hbox#coerce
+
     (** This method applies the new value of the parameter. *)
     method apply =
       let new_value = !value in
@@ -500,8 +511,10 @@ class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) =
   in
 
   object (self)
+
     (** This method returns the main box ready to be packed. *)
     method box = frame_selection#box#coerce
+
     (** This method applies the new value of the parameter. *)
     method apply =
       param.list_f_apply !listref ;
diff --git a/ide/coq.ml b/ide/coq.ml
index 88ffb4f0b7..91cd448eda 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -334,8 +334,8 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
     (* Parsing error at the end of s : we have only received a part of
         an xml answer. We store the current fragment for later *)
     let l_end = Lexing.lexeme_end lex in
-    (** Heuristic hack not to reimplement the lexer:  if ever the lexer dies
-        twice at the same place, then this is a non-recoverable error *)
+    (* Heuristic hack not to reimplement the lexer:  if ever the lexer dies
+       twice at the same place, then this is a non-recoverable error *)
     if state.lexerror = Some l_end then raise e;
     state.lexerror <- Some l_end
 
@@ -496,7 +496,7 @@ let init_coqtop coqtop task =
 type 'a query = 'a Interface.value task
 
 let eval_call call handle k =
-  (** Send messages to coqtop and prepare the decoding of the answer *)
+  (* Send messages to coqtop and prepare the decoding of the answer *)
   Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call);
   assert (handle.alive && handle.waiting_for = None);
   handle.waiting_for <- Some (mk_ccb (call,k));
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6c3438a4b0..8da9900724 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -255,8 +255,8 @@ object(self)
       let sentence = Doc.find document find in
       let mark = sentence.start in
       let iter = script#buffer#get_iter_at_mark mark in
-      (** Sentence starts tend to be at the end of a line, so we rather choose
-          the first non-line-ending position. *)
+      (* Sentence starts tend to be at the end of a line, so we rather choose
+         the first non-line-ending position. *)
       let rec sentence_start iter =
         if iter#ends_line then sentence_start iter#forward_line
         else iter
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 40b8d2f484..48c08899e0 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -566,7 +566,7 @@ let update_status sn =
   Coq.bind (Coq.status false) next
 
 let find_next_occurrence ~backward sn =
-  (** go to the next occurrence of the current word, forward or backward *)
+  (* go to the next occurrence of the current word, forward or backward *)
   let b = sn.buffer in
   let start = find_word_start (b#get_iter_at_mark `INSERT) in
   let stop = find_word_end start in
@@ -613,11 +613,11 @@ let printopts_callback opts v =
 (** Templates menu *)
 
 let get_current_word term =
-  (** First look to find if autocompleting *)
+  (* First look to find if autocompleting *)
   match term.script#complete_popup#proposal with
   | Some p -> p
   | None ->
-  (** Then look at the current selected word *)
+  (* Then look at the current selected word *)
   let buf1 = term.script#buffer in
   let buf2 = term.proof#buffer in
   if buf1#has_selection then
@@ -628,7 +628,7 @@ let get_current_word term =
     buf2#get_text ~slice:true ~start ~stop ()
   else if term.messages#has_selection then
     term.messages#get_selected_text
-  (** Otherwise try to find the word around the cursor *)
+  (* Otherwise try to find the word around the cursor *)
   else
     let it = term.script#buffer#get_iter_at_mark `INSERT in
     let start = find_word_start it in
@@ -772,11 +772,11 @@ let uncomment = cb_on_current_term (fun t -> t.script#uncomment ())
 let coqtop_arguments sn =
   let dialog = GWindow.dialog ~title:"Coqtop arguments" () in
   let coqtop = sn.coqtop in
-  (** Text entry *)
+  (* Text entry *)
   let args = Coq.get_arguments coqtop in
   let text = String.concat " " args in
   let entry = GEdit.entry ~text ~packing:dialog#vbox#add () in
-  (** Buttons *)
+  (* Buttons *)
   let box = dialog#action_area in
   let ok = GButton.button ~stock:`OK ~packing:box#add () in
   let ok_cb () =
diff --git a/ide/idetop.ml b/ide/idetop.ml
index a2b85041e8..8b3b566f9c 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -263,9 +263,9 @@ let wait () =
   set_doc (Stm.wait ~doc)
 
 let status force =
-  (** We remove the initial part of the current [DirPath.t]
-      (usually Top in an interactive session, cf "coqtop -top"),
-      and display the other parts (opened sections and modules) *)
+  (* We remove the initial part of the current [DirPath.t]
+     (usually Top in an interactive session, cf "coqtop -top"),
+     and display the other parts (opened sections and modules) *)
   set_doc (Stm.finish ~doc:(get_doc ()));
   if force then
     set_doc (Stm.join ~doc:(get_doc ()));
@@ -408,14 +408,12 @@ let interp ((_raw, verbose), s) =
 (** When receiving the Quit call, we don't directly do an [exit 0],
     but rather set this reference, in order to send a final answer
     before exiting. *)
-
 let quit = ref false
 
 (** Disabled *)
 let print_ast id = Xml_datatype.PCData "ERROR"
 
 (** Grouping all call handlers together + error handling *)
-
 let eval_call c =
   let interruptible f x =
     catch_break := true;
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 7044263b94..c14af7d21d 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -43,10 +43,10 @@ color on Windows.  A clean fix, if ever needed, would be to combine the attribut
 of the tags into a single composite tag before applying.  This is left as an
 exercise for the reader. *)
 let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
-  (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that
-      it has to reimplement its own helper function. Unluckily, it relies on
-      a slow algorithm, so that we have to have our own quicker version here.
-      Alas, it is still much slower than the native version... *)
+  (* FIXME: LablGTK2 does not export the C insert_with_tags function, so that
+     it has to reimplement its own helper function. Unluckily, it relies on
+     a slow algorithm, so that we have to have our own quicker version here.
+     Alas, it is still much slower than the native version... *)
   if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) text
   else
     let it = buf#get_iter_at_mark mark in
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index debbc8301e..ccb6bedaf6 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -78,16 +78,20 @@ type option_state = {
 }
 
 type search_constraint =
-(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
 | Name_Pattern of string
-(** Whether the object type satisfies a pattern *)
+(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
+
 | Type_Pattern of string
-(** Whether some subtype of object type satisfies a pattern *)
+(** Whether the object type satisfies a pattern *)
+
 | SubType_Pattern of string
-(** Whether the object pertains to a module *)
+(** Whether some subtype of object type satisfies a pattern *)
+
 | In_Module of string list
-(** Bypass the Search blacklist *)
+(** Whether the object pertains to a module *)
+
 | Include_Blacklist
+(** Bypass the Search blacklist *)
 
 (** A list of search constraints; the boolean flag is set to [false] whenever
     the flag should be negated. *)
diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml
index 19e9799c19..b2ce55e89a 100644
--- a/ide/protocol/richpp.ml
+++ b/ide/protocol/richpp.ml
@@ -46,7 +46,7 @@ let rich_pp width ppcmds =
   let pp_buffer = Buffer.create 180 in
 
   let push_pcdata () =
-    (** Push the optional PCData on the above node *)
+    (* Push the optional PCData on the above node *)
     let len = Buffer.length pp_buffer in
     if len = 0 then ()
     else match context.stack with
@@ -77,7 +77,7 @@ let rich_pp width ppcmds =
       let xml = Element (node, annotation, List.rev child) in
       match ctx with
       | Leaf ->
-        (** Final node: we keep the result in a dummy context *)
+        (* Final node: we keep the result in a dummy context *)
         context.stack <- Node ("", [xml], 0, Leaf)
       | Node (node, child, pos, ctx) ->
         context.stack <- Node (node, xml :: child, pos, ctx)
@@ -104,15 +104,15 @@ let rich_pp width ppcmds =
   pp_set_max_boxes ft 50 ;
   pp_set_ellipsis_text ft "...";
 
-  (** The whole output must be a valid document. To that
-      end, we nest the document inside <pp> tags. *)
+  (* The whole output must be a valid document. To that
+     end, we nest the document inside <pp> tags. *)
   pp_open_box ft 0;
   pp_open_tag ft "pp";
   Pp.(pp_with ft ppcmds);
   pp_close_tag ft ();
   pp_close_box ft ();
 
-  (** Get the resulting XML tree. *)
+  (* Get the resulting XML tree. *)
   let () = pp_print_flush ft () in
   let () = assert (Buffer.length pp_buffer = 0) in
   match context.stack with
diff --git a/ide/sentence.ml b/ide/sentence.ml
index 2f7820a77c..2e508969aa 100644
--- a/ide/sentence.ml
+++ b/ide/sentence.ml
@@ -91,8 +91,8 @@ let tag_on_insert buffer =
   in
   try
     let start = grab_sentence_start prev soi in
-    (** The status of "{" "}" as sentence delimiters is too fragile.
-        We retag up to the next "." instead. *)
+    (* The status of "{" "}" as sentence delimiters is too fragile.
+       We retag up to the next "." instead. *)
     let stop = grab_ending_dot insert in
     try split_slice_lax buffer start#backward_char stop
     with Coq_lex.Unterminated ->
diff --git a/ide/session.ml b/ide/session.ml
index be2bfe060c..805e1d38a7 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -217,7 +217,7 @@ let set_buffer_handlers
     | Some s -> Minilib.log (s^" moved")
     | None -> ()
   in
-  (** Pluging callbacks *)
+  (* Pluging callbacks *)
   let _ = buffer#connect#insert_text ~callback:insert_cb in
   let _ = buffer#connect#delete_range ~callback:delete_cb in
   let _ = buffer#connect#begin_user_action ~callback:begin_action_cb in
@@ -427,7 +427,7 @@ let build_layout (sn:session) =
     GPack.vbox ~packing:(session_paned#pack1 ~shrink:false ~resize:true) ()
   in
 
-  (** Right part of the window. *)
+  (* Right part of the window. *)
 
   let eval_paned = GPack.paned `HORIZONTAL ~border_width:5
     ~packing:(session_box#pack ~expand:true) () in
@@ -438,7 +438,7 @@ let build_layout (sn:session) =
   let state_paned = GPack.paned `VERTICAL
     ~packing:eval_paned#add2 () in
 
-  (** Proof buffer. *)
+  (* Proof buffer. *)
 
   let title = Printf.sprintf "Proof (%s)" sn.tab_label#text in
   let proof_detachable = Wg_Detachable.detachable ~title () in
@@ -454,7 +454,7 @@ let build_layout (sn:session) =
   let proof_scroll = GBin.scrolled_window
     ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_detachable#pack () in
 
-  (** Message buffer. *)
+  (* Message buffer. *)
 
   let message_frame = GPack.notebook ~packing:state_paned#add () in
   let add_msg_page pos name text (w : GObj.widget) =
@@ -514,14 +514,14 @@ let build_layout (sn:session) =
   let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#default_route#coerce in
   let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
   let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in
-  (** When a message is received, focus on the message pane *)
+  (* When a message is received, focus on the message pane *)
   let _ =
     sn.messages#default_route#connect#pushed ~callback:(fun _ _ ->
       let num = message_frame#page_num detach#coerce in
       if 0 <= num then message_frame#goto_page num
     )
   in
-  (** When an error occurs, paint the error label in red *)
+  (* When an error occurs, paint the error label in red *)
   let txt = label#text in
   let red s = "<span foreground=\"#FF0000\">" ^ s ^ "</span>" in
   sn.errpage#on_update ~callback:(fun l ->
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index 6a9317bc2f..c39d6d0563 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -40,7 +40,7 @@ let get_syntactic_completion (buffer : GText.buffer) pattern accu =
 (** Retrieve completion proposals in Coq libraries *)
 let get_semantic_completion pattern accu =
   let flags = [Interface.Name_Pattern ("^" ^ pattern), true] in
-  (** Only get the last part of the qualified name *)
+  (* Only get the last part of the qualified name *)
   let rec last accu = function
   | [] -> accu
   | [basename] -> Proposals.add basename accu
@@ -199,15 +199,15 @@ object (self)
           let () = self#init_proposals w props in
           update_completion_signal#call (start_offset, w, props)
         in
-        (** If not in the cache, we recompute it: first syntactic *)
+        (* If not in the cache, we recompute it: first syntactic *)
         let synt = get_syntactic_completion buffer w Proposals.empty in
-        (** Then semantic *)
+        (* Then semantic *)
         let next prop =
           let () = update prop in
           Coq.lift k
         in
         let query = Coq.bind (get_semantic_completion w synt) next in
-        (** If coqtop is computing, do the syntactic completion altogether *)
+        (* If coqtop is computing, do the syntactic completion altogether *)
         let occupied () =
           let () = update synt in
           k ()
@@ -264,20 +264,20 @@ object (self)
     renderer#set_properties [`FONT_DESC font; `XPAD 10]
 
   method private coordinates pos =
-    (** Toplevel position w.r.t. screen *)
+    (* Toplevel position w.r.t. screen *)
     let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in
-    (** Position of view w.r.t. window *)
+    (* Position of view w.r.t. window *)
     let (ux, uy) = Gdk.Window.get_position view#misc#window in
-    (** Relative buffer position to view *)
+    (* Relative buffer position to view *)
     let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in
-    (** Iter position *)
+    (* Iter position *)
     let iter = view#buffer#get_iter pos in
     let coords = view#get_iter_location iter in
     let lx = Gdk.Rectangle.x coords in
     let ly = Gdk.Rectangle.y coords in
     let w = Gdk.Rectangle.width coords in
     let h = Gdk.Rectangle.height coords in
-    (** Absolute position *)
+    (* Absolute position *)
     (x + lx + ux - dx, y + ly + uy - dy, w, h)
 
   method private select_any f =
@@ -374,9 +374,9 @@ object (self)
     else None
 
   method private manage_scrollbar () =
-    (** HACK: we don't have access to the treeview size because of the lack of
-        LablGTK binding for certain functions, so we bypass it by approximating
-        it through the size of the proposals *)
+    (* HACK: we don't have access to the treeview size because of the lack of
+       LablGTK binding for certain functions, so we bypass it by approximating
+       it through the size of the proposals *)
     let height = match model#store#get_iter_first with
     | None -> -1
     | Some iter ->
@@ -434,18 +434,18 @@ object (self)
         else false
       else false
     in
-    (** Style handling *)
+    (* Style handling *)
     let _ = view#misc#connect#style_set ~callback:self#refresh_style in
     let _ = self#refresh_style () in
     let _ = data#set_resize_mode `PARENT in
     let _ = frame#set_resize_mode `PARENT in
-    (** Callback to model *)
+    (* Callback to model *)
     let _ = model#connect#start_completion ~callback:self#start_callback in
     let _ = model#connect#update_completion ~callback:self#update_callback in
     let _ = model#connect#end_completion ~callback:self#end_callback in
-    (** Popup interaction *)
+    (* Popup interaction *)
     let _ = view#event#connect#key_press ~callback:key_cb in
-    (** Hiding the popup when necessary*)
+    (* Hiding the popup when necessary*)
     let _ = view#misc#connect#hide ~callback:obj#misc#hide in
     let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in
     let _ = view#connect#move_cursor ~callback:move_cb in
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 296a942321..7d2d7da570 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -212,13 +212,13 @@ class finder name (view : GText.view) =
     initializer
       let _ = self#hide () in
 
-      (** Widget button interaction *)
+      (* Widget button interaction *)
       let _ = next_button#connect#clicked ~callback:self#find_forward in
       let _ = previous_button#connect#clicked ~callback:self#find_backward in
       let _ = replace_button#connect#clicked ~callback:self#replace in
       let _ = replace_all_button#connect#clicked ~callback:self#replace_all in
 
-      (** Keypress interaction *)
+      (* Keypress interaction *)
       let generic_cb esc_cb ret_cb ev =
         let ev_key = GdkEvent.Key.keyval ev in
         let (return, _) = GtkData.AccelGroup.parse "Return" in
@@ -232,7 +232,7 @@ class finder name (view : GText.view) =
       let _ = find_entry#event#connect#key_press ~callback:find_cb in
       let _ = replace_entry#event#connect#key_press ~callback:replace_cb in
 
-      (** TextView interaction *)
+      (* TextView interaction *)
       let view_cb ev =
         if widget#visible then
           let ev_key = GdkEvent.Key.keyval ev in
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index a79a093e32..6b09b344b5 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -36,6 +36,7 @@ class type message_view =
     method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
+
     method has_selection : bool
     method get_selected_text : string
   end
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 472aaf5ed4..613f1b4190 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -26,6 +26,7 @@ class type message_view =
     method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
+
     method has_selection : bool
     method get_selected_text : string
   end
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 74bc0b8d53..5e26c50797 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -152,11 +152,11 @@ object(self)
     if self#process_delete_action del then (`OK, `WRITE) else (`FAIL, `NOOP)
   | Action lst ->
     let fold accu action = match accu with
-    | (`FAIL, _) -> accu (** we stop now! *)
+    | (`FAIL, _) -> accu (* we stop now! *)
     | (`OK, status) ->
       let (res, nstatus) = self#process_action action in
       let merge op1 op2 = match op1, op2 with
-      | `NOOP, `NOOP -> `NOOP (** only a noop when both are *)
+      | `NOOP, `NOOP -> `NOOP (* only a noop when both are *)
       | _ -> `WRITE
       in
       (res, merge status nstatus)
@@ -172,8 +172,8 @@ object(self)
     | (`OK, _) ->
       history <- rem;
       redo <- (negate_action action) :: redo
-    | (`FAIL, `NOOP) -> () (** we do nothing *)
-    | (`FAIL, `WRITE) -> self#clear_undo () (** we don't know how we failed, so start off *)
+    | (`FAIL, `NOOP) -> () (* we do nothing *)
+    | (`FAIL, `WRITE) -> self#clear_undo () (* we don't know how we failed, so start off *)
     end
 
   method perform_redo () = match redo with
@@ -184,8 +184,8 @@ object(self)
     | (`OK, _) ->
       redo <- rem;
       history <- (negate_action action) :: history;
-    | (`FAIL, `NOOP) -> () (** we do nothing *)
-    | (`FAIL, `WRITE) -> self#clear_undo () (** we don't know how we failed *)
+    | (`FAIL, `NOOP) -> () (* we do nothing *)
+    | (`FAIL, `WRITE) -> self#clear_undo () (* we don't know how we failed *)
     end
 
   method undo () =
@@ -212,9 +212,9 @@ object(self)
     self#with_lock_undo self#process_begin_user_action ()
 
   method process_end_user_action () =
-    (** Search for the pending action *)
+    (* Search for the pending action *)
     let rec split accu = function
-    | [] -> raise Not_found (** no pending begin action! *)
+    | [] -> raise Not_found (* no pending begin action! *)
     | EndGrp :: rem ->
       let grp = List.rev accu in
       let rec flatten = function
@@ -240,7 +240,7 @@ object(self)
     (* Save the insert action *)
     let len = Glib.Utf8.length s in
     let mergeable =
-      (** heuristic: split at newline and atomic pastes *)
+      (* heuristic: split at newline and atomic pastes *)
       len = 1 && (s <> "\n")
     in
     let ins = {
@@ -460,7 +460,7 @@ object (self)
       if not proceed then GtkSignal.stop_emit ()
     in
     let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
-    (** Plug on preferences *)
+    (* Plug on preferences *)
     let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed ~callback:cb in
     let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 0f5ed8d896..3b2572f9d2 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -70,7 +70,7 @@ object (self)
     let cb rect =
       let w = rect.Gtk.width in
       let h = rect.Gtk.height in
-      (** Only refresh when size actually changed, otherwise loops *)
+      (* Only refresh when size actually changed, otherwise loops *)
       if self#misc#visible && (width <> w || height <> h) then begin
         width <- w;
         height <- h;
@@ -91,7 +91,7 @@ object (self)
     let _ = eventbox#event#connect#button_press ~callback:clicked_cb in
     let cb show = if show then self#misc#show () else self#misc#hide () in
     stick show_progress_bar self cb;
-    (** Initial pixmap *)
+    (* Initial pixmap *)
     draw#set_pixmap pixmap;
     refresh_timer.Ideutils.run ~ms:300
       ~callback:(fun () -> if need_refresh then self#refresh (); true)
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 77d612cfd9..757d186c8b 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -80,8 +80,8 @@ type cases_pattern_expr_r =
 and cases_pattern_expr = cases_pattern_expr_r CAst.t
 
 and cases_pattern_notation_substitution =
-    cases_pattern_expr list *     (** for constr subterms *)
-    cases_pattern_expr list list  (** for recursive notations *)
+    cases_pattern_expr list *     (* for constr subterms *)
+    cases_pattern_expr list list  (* for recursive notations *)
 
 and constr_expr_r =
   | CRef     of qualid * instance_expr option
@@ -142,10 +142,10 @@ and local_binder_expr =
   | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
 
 and constr_notation_substitution =
-    constr_expr list *      (** for constr subterms *)
-    constr_expr list list * (** for recursive notations *)
-    cases_pattern_expr list *   (** for binders *)
-    local_binder_expr list list (** for binder lists (recursive notations) *)
+    constr_expr list *      (* for constr subterms *)
+    constr_expr list list * (* for recursive notations *)
+    cases_pattern_expr list *   (* for binders *)
+    local_binder_expr list list (* for binder lists (recursive notations) *)
 
 type constr_pattern_expr = constr_expr
 
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3a4969a3ee..3a5af1dd5f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 =
       in
       List.equal field_eq l1 l2
     | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
-      (** Don't care about the case_style *)
+      (* Don't care about the case_style *)
       Option.equal constr_expr_eq r1 r2 &&
       List.equal case_expr_eq a1 a2 &&
       List.equal branch_expr_eq brl1 brl2
@@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with
   | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
     eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
   | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
-    (** Don't care about the [binder_kind] *)
+    (* Don't care about the [binder_kind] *)
     List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
   | _ -> false
 
@@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with
   | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll))
 
 (** Folds and maps *)
-
 let is_constructor id =
   try Globnames.isConstructRef
         (Smartlocate.global_of_extended_global
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fba03b9de9..0d0b6158d9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -960,7 +960,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
 
   | GSort s -> CSort (extern_glob_sort s)
 
-  | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *)
+  | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *)
 
   | GCast (c, c') ->
       CCast (sub_extern true scopes vars c,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6313f2d7ba..40922b5c35 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1507,7 +1507,7 @@ let drop_notations_pattern looked_for genv =
   let test_kind top =
     if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
   in
-  (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+  (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
   let rec rcp_of_glob scopes x = DAst.(map (function
     | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
     | GHole (_,_,_) -> RCPatAtom (None)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 035e4bc644..61acd09d65 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -45,13 +45,15 @@ type var_internalization_type =
 
 type var_internalization_data =
     var_internalization_type *
-      (** type of the "free" variable, for coqdoc, e.g. while typing the
-	  constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+      (* type of the "free" variable, for coqdoc, e.g. while typing the
+         constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+
     Id.t list *
-      (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
-          in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
-    Impargs.implicit_status list * (** signature of impargs of the variable *)
-    Notation_term.scope_name option list (** subscopes of the args of the variable *)
+      (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+         in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+
+    Impargs.implicit_status list * (* signature of impargs of the variable *)
+    Notation_term.scope_name option list (* subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
 type internalization_env = var_internalization_data Id.Map.t
diff --git a/interp/declare.ml b/interp/declare.ml
index a809a856b9..a0ebc3775e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -56,7 +56,7 @@ let load_constant i ((sp,kn), obj) =
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn), obj) =
-  (** Never open a local definition *)
+  (* Never open a local definition *)
   if obj.cst_locl then ()
   else
     let con = Global.constant_of_delta_kn kn in
@@ -166,9 +166,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
         export_seff ||
         not de.const_entry_opaque ||
         is_poly de ->
-      (** This globally defines the side-effects in the environment. We mark
-          exported constants as being side-effect not to redeclare them at
-          caching time. *)
+      (* This globally defines the side-effects in the environment. We mark
+         exported constants as being side-effect not to redeclare them at
+         caching time. *)
       let de, export = Global.export_private_constants ~in_section de in
       export, ConstantEntry (PureEntry, DefinitionEntry de)
     | _ -> [], ConstantEntry (EffectEntry, cd)
@@ -191,7 +191,6 @@ let declare_definition ?(internal=UserIndividualRequest)
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of section variables and local definitions *)
-
 type section_variable_entry =
   | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
@@ -214,16 +213,16 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       let (de, eff) = Global.export_private_constants ~in_section:true de in
       let () = List.iter register_side_effect eff in
-      (** The body should already have been forced upstream because it is a
-          section-local definition, but it's not enforced by typing *)
+      (* The body should already have been forced upstream because it is a
+         section-local definition, but it's not enforced by typing *)
       let (body, uctx), () = Future.force de.const_entry_body in
       let poly, univs = match de.const_entry_universes with
       | Monomorphic_const_entry uctx -> false, uctx
       | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
       let univs = Univ.ContextSet.union uctx univs in
-      (** We must declare the universe constraints before type-checking the
-          term. *)
+      (* We must declare the universe constraints before type-checking the
+         term. *)
       let () = Global.push_context_set (not poly) univs in
       let se = {
         secdef_body = body;
@@ -262,7 +261,6 @@ let declare_variable id obj =
   oname
 
 (** Declaration of inductive blocks *)
-
 let declare_inductive_argument_scopes kn mie =
   List.iteri (fun i {mind_entry_consnames=lc} ->
     Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i));
@@ -360,7 +358,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
   let id = Label.to_id label in
   let univs = match univs with
     | Monomorphic_ind_entry _ ->
-      (** Global constraints already defined through the inductive *)
+      (* Global constraints already defined through the inductive *)
       Monomorphic_const_entry Univ.ContextSet.empty
     | Polymorphic_ind_entry (nas, ctx) ->
       Polymorphic_const_entry (nas, ctx)
@@ -511,7 +509,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
       load_function = load_univ_names;
       open_function = open_univ_names;
       discharge_function = discharge_univ_names;
-      subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
+      subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
 
 let declare_univ_binders gr pl =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 931d05a975..554da7603f 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -18,6 +18,7 @@ val dump : unit -> bool
 
 val noglob : unit -> unit
 val dump_into_file : string -> unit (** special handling of "stdout" *)
+
 val dump_to_dotglob : unit -> unit
 val feedback_glob : unit -> unit
 
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d024a9e808..8a89bcdf26 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -448,7 +448,7 @@ let compute_mib_implicits flags kn =
     Array.to_list
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
         (fun i mip ->
-	  (** No need to care about constraints here *)
+          (* No need to care about constraints here *)
           let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
 	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
         mib.mind_packets) in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ea5aa90f68..4afc2af5e9 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -65,6 +65,7 @@ type implicit_explanation =
      operational only if [conclusion_matters] is true. *)
 
 type maximal_insertion = bool (** true = maximal contextual insertion *)
+
 type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
 
 type implicit_status = (Id.t * implicit_explanation * 
diff --git a/interp/notation.ml b/interp/notation.ml
index 0af75b5bfa..e17cc65042 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -308,7 +308,7 @@ let declare_delimiters scope key =
     | None -> scope_map := String.Map.add scope newsc !scope_map
     | Some oldkey when String.equal oldkey key -> ()
     | Some oldkey ->
-        (** FIXME: implement multikey scopes? *)
+        (* FIXME: implement multikey scopes? *)
 	Flags.if_verbose Feedback.msg_info
 	  (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
 	scope_map := String.Map.add scope newsc !scope_map
diff --git a/interp/notation.mli b/interp/notation.mli
index 3480d1c8f2..ab0501a1e1 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool
 (** Open scope *)
 
 val open_close_scope :
-  (** locality *) bool * (* open *) bool * scope_name -> unit
+  (* locality *) bool * (* open *) bool * scope_name -> unit
 
 (** Extend a list of scopes *)
 val empty_scope_stack : scopes
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7a525f84a5..55a87fcd4d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -37,7 +37,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
    | _             -> false)
 | NApp (t1, a1), NApp (t2, a2) ->
   (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
-| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
+| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *)
 | NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
   Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
   (eq_notation_constr vars) u1 u2 && b1 == b2
@@ -51,7 +51,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
 | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
   Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
   Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
+| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
   let eqpat (p1, t1) (p2, t2) =
     List.equal cases_pattern_eq p1 p2 &&
     (eq_notation_constr vars) t1 t2
@@ -75,7 +75,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
   Option.equal (eq_notation_constr vars) o1 o2 &&
   (eq_notation_constr vars) u1 u2 &&
   (eq_notation_constr vars) r1 r2
-| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
+| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
   let eq (na1, o1, t1) (na2, o2, t2) =
     Name.equal na1 na2 &&
     Option.equal (eq_notation_constr vars) o1 o2 &&
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 5fb0ca1b43..0ef1f267f6 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -20,13 +20,13 @@ open Glob_term
     as well as non global expressions such as existential variables. *)
 
 type notation_constr =
-  (** Part common to [glob_constr] and [cases_pattern] *)
+  (* Part common to [glob_constr] and [cases_pattern] *)
   | NRef of GlobRef.t
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
-  (** Part only in [glob_constr] *)
+  (* Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
   | NProd of Name.t * notation_constr * notation_constr
   | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
diff --git a/kernel/.merlin.in b/kernel/.merlin.in
index 912ff61496..29da7d2cf6 100644
--- a/kernel/.merlin.in
+++ b/kernel/.merlin.in
@@ -1,4 +1,4 @@
-FLG -rectypes -thread -safe-string -w +a-4-44-50
+FLG -rectypes -thread -safe-string -w +a-4-44
 
 S ../clib
 B ../clib
diff --git a/lib/control.ml b/lib/control.ml
index 3fbeb168c4..e09068740d 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -62,8 +62,8 @@ let windows_timeout n f x e =
     let res = f x in
     let () = killed := true in
     let cur = Unix.gettimeofday () in
-    (** The thread did not interrupt, but the computation took longer than
-        expected. *)
+    (* The thread did not interrupt, but the computation took longer than
+       expected. *)
     let () = if float_of_int n <= cur -. init then begin
       exited := true;
       raise Sys.Break
@@ -71,7 +71,7 @@ let windows_timeout n f x e =
     res
   with
   | Sys.Break ->
-    (** Just in case, it could be a regular Ctrl+C *)
+    (* Just in case, it could be a regular Ctrl+C *)
     if not !exited then begin killed := true; raise Sys.Break end
     else raise e
   | e ->
diff --git a/lib/system.mli b/lib/system.mli
index f13fd30923..a3b79ee528 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -102,6 +102,7 @@ type time
 
 val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
+
 val fmt_time_difference : time -> time -> Pp.t
 
 val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 351a0a7e84..f6779dbbde 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -190,12 +190,18 @@ val build_bool_type : coq_bool_data delayed
 val build_prod : coq_sigma_data delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
 
-val build_coq_eq       : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq       : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
-val build_coq_eq_refl  : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *)
+(** = [(build_coq_eq_data()).eq] *)
+
+val build_coq_eq_refl  : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
-val build_coq_eq_sym   : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *)
+(** = [(build_coq_eq_data()).refl] *)
+
+val build_coq_eq_sym   : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
+(** = [(build_coq_eq_data()).sym] *)
+
 val build_coq_f_equal2 : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
 
@@ -222,8 +228,8 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 val build_coq_sumbool : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
 
-(** {6 ... } *)
-(** Connectives
+(** {6 ... }
+   Connectives
    The False proposition *)
 val build_coq_False : GlobRef.t delayed
 [@@ocaml.deprecated "Please use Coqlib.lib_ref"]
diff --git a/library/decls.mli b/library/decls.mli
index 401884736e..c0db537427 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-  DirPath.t * bool (** opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
+  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
diff --git a/library/goptions.ml b/library/goptions.ml
index 98efb512ab..340d74151b 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -246,14 +246,14 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
       | OptGlobal -> cache_options o
       | OptExport -> ()
       | OptLocal | OptDefault ->
-        (** Ruled out by classify_function *)
+        (* Ruled out by classify_function *)
         assert false
       in
       let open_options i  (_, (l, _, _) as o) = match l with
       | OptExport -> if Int.equal i 1 then cache_options o
       | OptGlobal -> ()
       | OptLocal | OptDefault ->
-        (** Ruled out by classify_function *)
+        (* Ruled out by classify_function *)
         assert false
       in
       let subst_options (subst,obj) = obj in
diff --git a/library/lib.ml b/library/lib.ml
index 9c13cdafdb..cce5feeb4a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -481,8 +481,8 @@ let named_of_variable_context =
   List.map fst
 
 let name_instance inst =
-  (** FIXME: this should probably be done at an upper level, by storing the
-      name information in the section data structure. *)
+  (* FIXME: this should probably be done at an upper level, by storing the
+     name information in the section data structure. *)
   let map lvl = match Univ.Level.name lvl with
     | None -> (* Having Prop/Set/Var as section universes makes no sense *)
       assert false
@@ -491,8 +491,8 @@ let name_instance inst =
         let qid = Nametab.shortest_qualid_of_universe na in
         Name (Libnames.qualid_basename qid)
       with Not_found ->
-        (** Best-effort naming from the string representation of the level.
-            See univNames.ml for a similar hack. *)
+        (* Best-effort naming from the string representation of the level.
+           See univNames.ml for a similar hack. *)
         Name (Id.of_string_soft (Univ.Level.to_string lvl))
   in
   Array.map map (Univ.Instance.to_array inst)
diff --git a/library/libnames.mli b/library/libnames.mli
index 9960603cbb..bbb4d2a058 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -94,8 +94,8 @@ val qualid_basename : qualid -> Id.t
 val default_library : DirPath.t
 
 (** This is the root of the standard library of Coq *)
-val coq_root : module_ident (** "Coq" *)
-val coq_string : string (** "Coq" *)
+val coq_root : module_ident (* "Coq" *)
+val coq_string : string (* "Coq" *)
 
 (** This is the default root prefix for developments which doesn't
    mention a root *)
diff --git a/library/library.mli b/library/library.mli
index d298a371b5..c016352808 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -19,8 +19,8 @@ open Libnames
   written at various dates.
 *)
 
-(** {6 ... } *)
-(** Require = load in the environment + open (if the optional boolean
+(** {6 ... }
+    Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
 
diff --git a/library/nametab.ml b/library/nametab.ml
index f0f643d9b5..95890b2edf 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -107,6 +107,7 @@ module type NAMETREE = sig
   val user_name : qualid -> t -> user_name
   val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
+
   (** Matches a prefix of [qualid], useful for completion *)
   val match_prefixes : qualid -> t -> elt list
 end
diff --git a/library/nametab.mli b/library/nametab.mli
index b7926cf515..fccb8fd918 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -171,7 +171,9 @@ val exists_cci : full_path -> bool
 val exists_modtype : full_path -> bool
 val exists_dir : DirPath.t -> bool
 val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+
 val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+
 val exists_universe : full_path -> bool
 
 (** {6 These functions locate qualids into full user names } *)
diff --git a/library/summary.ml b/library/summary.ml
index 9b22945919..b68f1fb01b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -92,7 +92,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
   | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
   | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
   end;
-  (** We must be independent on the order of the map! *)
+  (* We must be independent on the order of the map! *)
   let ufz name decl =
     try decl.unfreeze_function String.Map.(find name summaries)
     with Not_found ->
diff --git a/library/summary.mli b/library/summary.mli
index 7d91a79188..64222761ba 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -19,9 +19,9 @@ type marshallable =
 (** Types of global Coq states. The ['a] type should be pure and marshallable by
     the standard OCaml marshalling function. *)
 type 'a summary_declaration = {
-  (** freeze_function [true] is for marshalling to disk. 
-   *  e.g. lazy must be forced *)
   freeze_function : marshallable -> 'a;
+  (** freeze_function [true] is for marshalling to disk.
+   *  e.g. lazy must be forced *)
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 050ed49622..9b5537d7f6 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -106,11 +106,11 @@ type 'a production_rule =
 
 type 'a single_extend_statement =
   string option *
-  (** Level *)
+  (* Level *)
   Gramlib.Gramext.g_assoc option *
-  (** Associativity *)
+  (* Associativity *)
   'a production_rule list
-  (** Symbol list with the interpretation function *)
+  (* Symbol list with the interpretation function *)
 
 type 'a extend_statement =
   Gramlib.Gramext.position option *
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 9b8c008555..55fcd33272 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -27,6 +27,7 @@ val to_string : t -> string
 (* Needed to fit Camlp5 signature *)
 val print : Format.formatter -> t -> unit
 val match_keyword : string -> t -> bool
+
 (** for camlp5 *)
 val of_pattern : string*string -> t
 val to_pattern : t -> string*string
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 480819ebe1..6f9384941b 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -27,12 +27,12 @@ let start_deriving f suchthat lemma =
   let sigma = Evd.from_env env in
   let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
 
-  (** create a sort variable for the type of [f] *)
+  (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
      that looked the most general. *)
   let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
   let f_type_type = EConstr.mkSort f_type_sort in
-  (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
+  (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
   let goals =
     let open Proofview in
         TCons ( env , sigma , f_type_type , (fun sigma f_type ->
@@ -45,14 +45,14 @@ let start_deriving f suchthat lemma =
         TNil sigma))))))
     in
 
-    (** The terminator handles the registering of constants when the proof is closed. *)
+    (* The terminator handles the registering of constants when the proof is closed. *)
     let terminator com =
       let open Proof_global in
-      (** Extracts the relevant information from the proof. [Admitted]
-          and [Save] result in user errors. [opaque] is [true] if the
-          proof was concluded by [Qed], and [false] if [Defined]. [f_def]
-          and [lemma_def] correspond to the proof of [f] and of
-          [suchthat], respectively. *)
+      (* Extracts the relevant information from the proof. [Admitted]
+         and [Save] result in user errors. [opaque] is [true] if the
+         proof was concluded by [Qed], and [false] if [Defined]. [f_def]
+         and [lemma_def] correspond to the proof of [f] and of
+         [suchthat], respectively. *)
       let (opaque,f_def,lemma_def) =
         match com with
         | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
@@ -64,26 +64,26 @@ let start_deriving f suchthat lemma =
                 opaque <> Proof_global.Transparent , f_def , lemma_def
             | _ -> assert false
       in
-      (** The opacity of [f_def] is adjusted to be [false], as it
-          must. Then [f] is declared in the global environment. *)
+      (* The opacity of [f_def] is adjusted to be [false], as it
+         must. Then [f] is declared in the global environment. *)
       let f_def = { f_def with Entries.const_entry_opaque = false } in
       let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
       let f_kn = Declare.declare_constant f f_def in
       let f_kn_term = mkConst f_kn in
-      (** In the type and body of the proof of [suchthat] there can be
-          references to the variable [f]. It needs to be replaced by
-          references to the constant [f] declared above. This substitution
-          performs this precise action. *)
+      (* In the type and body of the proof of [suchthat] there can be
+         references to the variable [f]. It needs to be replaced by
+         references to the constant [f] declared above. This substitution
+         performs this precise action. *)
       let substf c = Vars.replace_vars [f,f_kn_term] c in
-      (** Extracts the type of the proof of [suchthat]. *)
+      (* Extracts the type of the proof of [suchthat]. *)
       let lemma_pretype =
         match Entries.(lemma_def.const_entry_type) with
         | Some t -> t
         | None -> assert false (* Proof_global always sets type here. *)
       in
-      (** The references of [f] are subsituted appropriately. *)
+      (* The references of [f] are subsituted appropriately. *)
       let lemma_type = substf lemma_pretype in
-      (** The same is done in the body of the proof. *)
+      (* The same is done in the body of the proof. *)
       let lemma_body =
         map_const_entry_body substf Entries.(lemma_def.const_entry_body)
       in
@@ -105,7 +105,3 @@ let start_deriving f suchthat lemma =
     Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
   end in
   ()
-
-
-
-
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index 9c0f373c6a..c675eacc92 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.ml
@@ -20,8 +20,10 @@ type big_int = Big_int.big_int
 
 let zero = zero_big_int
         (** The big integer [0]. *)
+
 let one = unit_big_int
         (** The big integer [1]. *)
+
 let two = big_int_of_int 2
         (** The big integer [2]. *)
 
@@ -29,28 +31,39 @@ let two = big_int_of_int 2
 
 let opp = minus_big_int
         (** Unary negation. *)
+
 let abs = abs_big_int
         (** Absolute value. *)
+
 let add = add_big_int
         (** Addition. *)
+
 let succ = succ_big_int
         (** Successor (add 1). *)
+
 let add_int = add_int_big_int
         (** Addition of a small integer to a big integer. *)
+
 let sub = sub_big_int
         (** Subtraction. *)
+
 let pred = pred_big_int
         (** Predecessor (subtract 1). *)
+
 let mult = mult_big_int
         (** Multiplication of two big integers. *)
+
 let mult_int = mult_int_big_int
         (** Multiplication of a big integer by a small integer *)
+
 let square = square_big_int
         (** Return the square of the given big integer *)
+
 let sqrt = sqrt_big_int
         (** [sqrt_big_int a] returns the integer square root of [a],
            that is, the largest big integer [r] such that [r * r <= a].
            Raise [Invalid_argument] if [a] is negative. *)
+
 let quomod = quomod_big_int
         (** Euclidean division of two big integers.
            The first part of the result is the quotient,
@@ -58,14 +71,18 @@ let quomod = quomod_big_int
            Writing [(q,r) = quomod_big_int a b], we have
            [a = q * b + r] and [0 <= r < |b|].
            Raise [Division_by_zero] if the divisor is zero. *)
+
 let div = div_big_int
         (** Euclidean quotient of two big integers.
            This is the first result [q] of [quomod_big_int] (see above). *)
+
 let modulo = mod_big_int
         (** Euclidean modulus of two big integers.
            This is the second result [r] of [quomod_big_int] (see above). *)
+
 let gcd = gcd_big_int
         (** Greatest common divisor of two big integers. *)
+
 let power = power_big_int_positive_big_int
         (** Exponentiation functions.  Return the big integer
            representing the first argument [a] raised to the power [b]
@@ -78,18 +95,22 @@ let power = power_big_int_positive_big_int
 let sign = sign_big_int
         (** Return [0] if the given big integer is zero,
            [1] if it is positive, and [-1] if it is negative. *)
+
 let compare = compare_big_int
         (** [compare_big_int a b] returns [0] if [a] and [b] are equal,
            [1] if [a] is greater than [b], and [-1] if [a] is smaller
            than [b]. *)
+
 let eq = eq_big_int
 let le = le_big_int
 let ge = ge_big_int
 let lt = lt_big_int
 let gt = gt_big_int
         (** Usual boolean comparisons between two big integers. *)
+
 let max = max_big_int
         (** Return the greater of its two arguments. *)
+
 let min = min_big_int
         (** Return the smaller of its two arguments. *)
 
@@ -98,6 +119,7 @@ let min = min_big_int
 let to_string = string_of_big_int
         (** Return the string representation of the given big integer,
            in decimal (base 10). *)
+
 let of_string = big_int_of_string
         (** Convert a string to a big integer, in decimal.
            The string consists of an optional [-] or [+] sign,
@@ -107,6 +129,7 @@ let of_string = big_int_of_string
 
 let of_int = big_int_of_int
         (** Convert a small integer to a big integer. *)
+
 let is_int = is_int_big_int
         (** Test whether the given big integer is small enough to
            be representable as a small integer (type [int])
@@ -115,6 +138,7 @@ let is_int = is_int_big_int
            [a] is between 2{^30} and 2{^30}-1.  On a 64-bit platform,
            [is_int_big_int a] returns [true] if and only if
            [a] is between -2{^62} and 2{^62}-1. *)
+
 let to_int = int_of_big_int
         (** Convert a big integer to a small integer (type [int]).
            Raises [Failure "int_of_big_int"] if the big integer
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index bdeb6fca60..59c57cc544 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -125,7 +125,7 @@ module KOrd =
 struct
   type t = kind * string
   let compare (k1, s1) (k2, s2) =
-    let c = Pervasives.compare k1 k2 (** OK *) in
+    let c = Pervasives.compare k1 k2 (* OK *) in
     if c = 0 then String.compare s1 s2
     else c
 end
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 4cdfc6fac5..12b68e208c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -41,7 +41,7 @@ let pop t = Vars.lift (-1) t
 *)
 let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let princ_type = EConstr.of_constr princ_type in
-  let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in
+  let princ_type_info = compute_elim_sig Evd.empty princ_type (* FIXME *) in
   let env = Global.env () in
   let env_with_params = EConstr.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 603dd60cf2..ec2adf065a 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -306,8 +306,8 @@ let add_rewrite_hint ~poly bases ort t lcsr =
     let ctx =
       let ctx = UState.context_set ctx in
         if poly then ctx
-	else (** This is a global universe context that shouldn't be
-	       refreshed at every use of the hint, declare it globally. *)
+	else (* This is a global universe context that shouldn't be
+	        refreshed at every use of the hint, declare it globally. *)
 	  (Declare.declare_universe_context false ctx;
            Univ.ContextSet.empty)
     in
@@ -738,7 +738,8 @@ let  mkCaseEq a  : unit Proofview.tactic =
           Proofview.Goal.enter begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
-            (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
+            (* FIXME: this looks really wrong. Does anybody really use
+               this tactic? *)
             let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
 	    change_concl c
           end;
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index ef18dd6cdc..1ea6ff84d4 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -24,7 +24,7 @@ let (set_default_tactic, get_default_tactic, print_default_tactic) =
   Tactic_option.declare_tactic_option "Program tactic"
 
 let () =
-  (** Delay to recover the tactic imperatively *)
+  (* Delay to recover the tactic imperatively *)
   let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
     snd (get_default_tactic ())
   end in
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 55e58187b0..2267d43d93 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -235,8 +235,8 @@ let string_of_genarg_arg (ArgumentType arg) =
   let pr_tacarg_using_rule pr_gen l =
     let l = match l with
     | TacTerm s :: l ->
-      (** First terminal token should be considered as the name of the tactic,
-          so we tag it differently than the other terminal tokens. *)
+      (* First terminal token should be considered as the name of the tactic,
+         so we tag it differently than the other terminal tokens. *)
       primitive s :: tacarg_using_rule_token pr_gen l
     | _ -> tacarg_using_rule_token pr_gen l
     in
@@ -1180,7 +1180,7 @@ let pr_goal_selector ~toplevel s =
         pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
-        (** Those are not used by the atomic printer *)
+        (* Those are not used by the atomic printer *)
         pr_generic = (fun _ -> assert false);
         pr_extend = (fun _ _ _ -> assert false);
         pr_alias = (fun _ _ _ -> assert false);
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 06783de614..e626df5579 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -97,7 +97,7 @@ let goalevars evars = fst evars
 let cstrevars evars = snd evars
 
 let new_cstr_evar (evd,cstrs) env t =
-  (** We handle the typeclass resolution of constraints ourselves *)
+  (* We handle the typeclass resolution of constraints ourselves *)
   let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in
   let ev, _ = destEvar evd' t in
     (evd', Evar.Set.add ev cstrs), t
@@ -474,7 +474,7 @@ let get_symmetric_proof b =
 let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
 
 let rec decompose_app_rel env evd t = 
-  (** Head normalize for compatibility with the old meta mechanism *)
+  (* Head normalize for compatibility with the old meta mechanism *)
   let t = Reductionops.whd_betaiota evd t in
   match EConstr.kind evd t with
   | App (f, [||]) -> assert false
@@ -613,7 +613,7 @@ let solve_remaining_by env sigma holes by =
         Some evk
       | _ -> None
     in
-    (** Only solve independent holes *)
+    (* Only solve independent holes *)
     let indep = List.map_filter map holes in
     let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
     let solve_tac = match tac with
@@ -628,7 +628,7 @@ let solve_remaining_by env sigma holes by =
       in
       match evi with
       | None -> sigma
-        (** Evar should not be defined, but just in case *)
+        (* Evar should not be defined, but just in case *)
       | Some evi ->
         let env = Environ.reset_with_named_context evi.evar_hyps env in
         let ty = evi.evar_concl in
@@ -646,6 +646,7 @@ let poly_inverse sort =
 type rewrite_proof = 
   | RewPrf of constr * constr
   (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)
+
   | RewCast of cast_kind
   (** A proof of convertibility (with casts) *)
 
@@ -1561,7 +1562,7 @@ let newfail n s =
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
-  (** For compatibility *)
+  (* For compatibility *)
   let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
   let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
   let treat sigma res = 
@@ -1611,7 +1612,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
     let env = match clause with
     | None -> env
     | Some id ->
-      (** Only consider variables not depending on [id] *)
+      (* Only consider variables not depending on [id] *)
       let ctx = named_context env in
       let filter decl = not (occur_var_in_decl env sigma id decl) in
       let nctx = List.filter filter ctx in
@@ -1623,7 +1624,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
       in
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
       treat sigma res <*>
-      (** For compatibility *)
+      (* For compatibility *)
       beta <*> Proofview.shelve_unifiable
     with
     | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2aee809eb6..b770b97384 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -169,7 +169,7 @@ let add_tactic_entry (kn, ml, tg) state =
   let entry, pos = get_tactic_entry tg.tacgram_level in
   let mkact loc l =
     let map arg =
-      (** HACK to handle especially the tactic(...) entry *)
+      (* HACK to handle especially the tactic(...) entry *)
       let wit = Genarg.rawwit Tacarg.wit_tactic in
       if Genarg.has_type arg wit && not ml then
         Tacexp (Genarg.out_gen wit arg)
@@ -223,7 +223,7 @@ let interp_prod_item = function
       | Some arg -> arg
       end
     | Some n ->
-      (** FIXME: do better someday *)
+      (* FIXME: do better someday *)
       assert (String.equal s "tactic");
       begin match Tacarg.wit_tactic with
       | ExtraArg tag -> ArgT.Any tag
@@ -241,9 +241,9 @@ let make_fresh_key =
     | TacNonTerm _ -> "#"
     in
     let prods = String.concat "_" (List.map map prods) in
-    (** We embed the hash of the kernel name in the label so that the identifier
-        should be mostly unique. This ensures that including two modules
-        together won't confuse the corresponding labels. *)
+    (* We embed the hash of the kernel name in the label so that the identifier
+       should be mostly unique. This ensures that including two modules
+       together won't confuse the corresponding labels. *)
     let hash = (cur lxor (ModPath.hash (Lib.current_mp ()))) land 0x7FFFFFFF in
     let lbl = Id.of_string_soft (Printf.sprintf "%s_%08X" prods hash) in
     Lib.make_kn lbl
@@ -281,7 +281,7 @@ let open_tactic_notation i (_, tobj) =
 let load_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
   let () = check_key key in
-  (** Only add the printing and interpretation rules. *)
+  (* Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram);
   if Int.equal i 1 && not tobj.tacobj_local then
@@ -342,7 +342,7 @@ let extend_atomic_tactic name entries =
   let map_prod prods =
     let (hd, rem) = match prods with
     | TacTerm s :: rem -> (s, rem)
-    | _ -> assert false (** Not handled by the ML extension syntax *)
+    | _ -> assert false (* Not handled by the ML extension syntax *)
     in
     let empty_value = function
     | TacTerm s -> raise NonEmptyArgument
@@ -383,8 +383,8 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
     add_glob_tactic_notation false ~level ?deprecation prods true ids tac
   in
   List.iteri iter (List.rev prods);
-  (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
-  tactic_expr level 0) *)
+  (* We call [extend_atomic_tactic] only for "basic tactics" (the ones
+     at tactic_expr level 0) *)
   if Int.equal level 0 then extend_atomic_tactic name prods
 
 (**********************************************************************)
@@ -474,8 +474,9 @@ let register_ltac local ?deprecation tacl =
     (name, body)
   in
   let defs () =
-    (** Register locally the tactic to handle recursivity. This function affects
-        the whole environment, so that we transactify it afterwards. *)
+    (* Register locally the tactic to handle recursivity. This
+       function affects the whole environment, so that we transactify
+       it afterwards. *)
     let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in
     let () = List.iter iter_rec recvars in
     List.map map rfun
@@ -557,7 +558,7 @@ let () =
   register_grammars_by_name "tactic" entries
 
 let get_identifier i =
-  (** Workaround for badly-designed generic arguments lacking a closure *)
+  (* Workaround for badly-designed generic arguments lacking a closure *)
   Names.Id.of_string_soft (Printf.sprintf "$%i" i)
 
 type _ ty_sig =
@@ -650,20 +651,22 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
   in
   match sign with
   | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s ->
-  (** The extension is only made of a name followed by constr entries: we do not
-      add any grammar nor printing rule and add it as a true Ltac definition. *)
+    (* The extension is only made of a name followed by constr
+       entries: we do not add any grammar nor printing rule and add it
+       as a true Ltac definition. *)
     let vars = mk_sign_vars 1 s in
     let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in
     let tac = match s with
     | TyNil -> eval ml_tac
-    (** Special handling of tactics without arguments: such tactics do not do
-        a Proofview.Goal.nf_enter to compute their arguments. It matters for some
-        whole-prof tactics like [shelve_unifiable]. *)
+    (* Special handling of tactics without arguments: such tactics do
+       not do a Proofview.Goal.nf_enter to compute their arguments. It
+       matters for some whole-prof tactics like [shelve_unifiable]. *)
     | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac)
     in
-  (** Arguments are not passed directly to the ML tactic in the TacML node,
-      the ML tactic retrieves its arguments in the [ist] environment instead.
-      This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
+    (* Arguments are not passed directly to the ML tactic in the TacML
+       node, the ML tactic retrieves its arguments in the [ist]
+       environment instead.  This is the rôle of the
+       [lift_constr_tac_to_ml_tac] function. *)
     let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, [])))in
     let id = Names.Id.of_string name in
     let obj () = Tacenv.register_ltac true false id body ?deprecation in
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 2bd21f9d7a..83f563e2ab 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -78,12 +78,12 @@ type ('a,'t) match_rule =
 
 (** Extension indentifiers for the TACTIC EXTEND mechanism. *)
 type ml_tactic_name = {
+  mltac_plugin : string;
   (** Name of the plugin where the tactic is defined, typically coming from a
       DECLARE PLUGIN statement in the source. *)
-  mltac_plugin : string;
+  mltac_tactic : string;
   (** Name of the tactic entry where the tactic is defined, typically found
       after the TACTIC EXTEND statement in the source. *)
-  mltac_tactic : string;
 }
 
 type ml_tactic_entry = {
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 0c27f3bfe2..da0ecfc449 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -78,12 +78,12 @@ type ('a,'t) match_rule =
 
 (** Extension indentifiers for the TACTIC EXTEND mechanism. *)
 type ml_tactic_name = {
+  mltac_plugin : string;
   (** Name of the plugin where the tactic is defined, typically coming from a
       DECLARE PLUGIN statement in the source. *)
-  mltac_plugin : string;
+  mltac_tactic : string;
   (** Name of the tactic entry where the tactic is defined, typically found
       after the TACTIC EXTEND statement in the source. *)
-  mltac_tactic : string;
 }
 
 type ml_tactic_entry = {
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 85c6348b52..a1e21aab04 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -843,8 +843,9 @@ let notation_subst bindings tac =
     (make ?loc @@ Name id, c) :: accu
   in
   let bindings = Id.Map.fold fold bindings [] in
-  (** This is theoretically not correct due to potential variable capture, but
-      Ltac has no true variables so one cannot simply substitute *)
+  (* This is theoretically not correct due to potential variable
+     capture, but Ltac has no true variables so one cannot simply
+     substitute *)
   TacLetIn (false, bindings, tac)
 
 let () = Genintern.register_ntn_subst0 wit_tactic notation_subst
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index cf5eb442be..284642b38c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -50,7 +50,7 @@ let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v w
   let Val.Dyn (t, _) = v in
   let t' = match val_tag wit with
   | Val.Base t' -> t'
-  | _ -> assert false (** not used in this module *)
+  | _ -> assert false (* not used in this module *)
   in
   match Val.eq t t' with
   | None -> false
@@ -68,13 +68,13 @@ let in_list tag v =
 let in_gen wit v =
   let t = match val_tag wit with
   | Val.Base t -> t
-  | _ -> assert false (** not used in this module *)
+  | _ -> assert false (* not used in this module *)
   in
   Val.Dyn (t, v)
 let out_gen wit v =
   let t = match val_tag wit with
   | Val.Base t -> t
-  | _ -> assert false (** not used in this module *)
+  | _ -> assert false (* not used in this module *)
   in
   match prj t v with None -> assert false | Some x -> x
 
@@ -585,8 +585,8 @@ let interp_pure_open_constr ist =
 let interp_typed_pattern ist env sigma (_,c,_) =
   let sigma, c =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
-  (** FIXME: it is necessary to be unsafe here because of the way we handle
-      evars in the pretyper. Sometimes they get solved eagerly. *)
+  (* FIXME: it is necessary to be unsafe here because of the way we handle
+     evars in the pretyper. Sometimes they get solved eagerly. *)
   pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
 
 (* Interprets a constr expression *)
@@ -897,7 +897,7 @@ let interp_destruction_arg ist gl arg =
           end)
       in
       try
-        (** FIXME: should be moved to taccoerce *)
+        (* FIXME: should be moved to taccoerce *)
         let v = Id.Map.find id ist.lfun in
         if has_type v (topwit wit_intro_pattern) then
           let v = out_gen (topwit wit_intro_pattern) v in
@@ -1020,7 +1020,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
   | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr
   | TacArg {loc;v} -> interp_tacarg ist v
   | t ->
-    (** Delayed evaluation *)
+    (* Delayed evaluation *)
     Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t)))
   in
   let open Ftactic in
@@ -1396,12 +1396,12 @@ and interp_match_successes lz ist s =
         general
     | Select ->
       begin
-        (** Only keep the first matching result, we don't backtrack on it *)
+        (* Only keep the first matching result, we don't backtrack on it *)
         let s = Proofview.tclONCE s in
         s >>= fun ans -> interp_match_success ist ans
       end
     | Once ->
-        (** Once a tactic has succeeded, do not backtrack anymore *)
+        (* Once a tactic has succeeded, do not backtrack anymore *)
         Proofview.tclONCE general
 
 (* Interprets the Match expressions *)
@@ -1438,7 +1438,7 @@ and interp_match_goal ist lz lr lmr =
 (* Interprets extended tactic generic arguments *)
 and interp_genarg ist x : Val.t Ftactic.t =
     let open Ftactic.Notations in
-    (** Ad-hoc handling of some types. *)
+    (* Ad-hoc handling of some types. *)
     let tag = genarg_tag x in
     if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then
       interp_genarg_var_list ist x
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index c949589e22..54924f1644 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -59,7 +59,7 @@ let id_map_try_add_name id x m =
     the binding of the right-hand argument shadows that of the left-hand
     argument. *)
 let id_map_right_biased_union m1 m2 =
-  if Id.Map.is_empty m1 then m2 (** Don't reconstruct the whole map *)
+  if Id.Map.is_empty m1 then m2 (* Don't reconstruct the whole map *)
   else Id.Map.fold Id.Map.add m2 m1
 
 (** Tests whether the substitution [s] is empty. *)
@@ -102,7 +102,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
         else raise Not_coherent_metas
   in
   let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 in
-  (** ppedrot: Is that even correct? *)
+  (* ppedrot: Is that even correct? *)
   let merged = ln +++ ln1 in
   (merged, Id.Map.merge merge lcm lm)
 
@@ -263,8 +263,8 @@ module PatternMatching (E:StaticEnvironment) = struct
     | All lhs -> wildcard_match_term lhs
     | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs
     | Pat _ ->
-        (** Rules with hypotheses, only work in match goal. *)
-        fail
+      (* Rules with hypotheses, only work in match goal. *)
+      fail
 
   (** [match_term term rules] matches the term [term] with the set of
       matching rules [rules].*)
diff --git a/plugins/micromega/itv.ml b/plugins/micromega/itv.ml
index dc1df7ec9f..44cad820ed 100644
--- a/plugins/micromega/itv.ml
+++ b/plugins/micromega/itv.ml
@@ -11,10 +11,11 @@
 (** Intervals (extracted from mfourier.ml) *)
 
 open Num
+
   (** The type of intervals is *)
   type interval = num option * num option
-      (** None models the absence of bound i.e. infinity *)
-      (** As a result,
+      (** None models the absence of bound i.e. infinity
+          As a result,
           - None , None   -> \]-oo,+oo\[
           - None , Some v -> \]-oo,v\]
           - Some v, None  -> \[v,+oo\[
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index f5e9a9f34c..23f3470d77 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -103,7 +103,7 @@ module Poly : sig
 
 end
 
-type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (** Representation of linear constraints *)
+type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (* Representation of linear constraints *)
 and op = Eq | Ge | Gt
 
 val eval_op : op -> Num.num -> Num.num -> bool
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index 8d8c6ea90b..4465aa1ee1 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -20,6 +20,7 @@ type iset = unit IMap.t
 
 type tableau = Vect.t IMap.t (** Mapping basic variables to their equation.
                                  All variables >= than a threshold rst are restricted.*)
+
 module Restricted =
   struct
     type t =
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index f8fc943713..1825a4d77c 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -609,7 +609,7 @@ type current_problem = {
 exception NotInIdealUpdate of current_problem
 
 let test_dans_ideal cur_pb table metadata p lp len0 =
-  (** Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *)
+  (* Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *)
   let (c,r) = reduce2 table cur_pb.cur_poly lp in
   info (fun () -> "remainder: "^(stringPcut metadata r));
   let cur_pb = {
@@ -657,7 +657,7 @@ let deg_hom p =
   | (a,m)::_ -> Monomial.deg m
 
 let pbuchf table metadata cur_pb homogeneous (lp, lpc) p =
-  (** Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *)
+  (* Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *)
   sinfo "computation of the Groebner basis";
   let () = match table.hmon with
   | None -> ()
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index ef60a23e80..1777418ef6 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -374,7 +374,7 @@ let remove_zeros lci =
   let m = List.length lci in
   let u = Array.make m false in
   let rec utiles k =
-    (** TODO: Find a more reasonable implementation of this traversal. *)
+    (* TODO: Find a more reasonable implementation of this traversal. *)
     if k >= m || u.(k) then ()
     else
       let () = u.(k) <- true in
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index e66fa10d5b..f1fa694356 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -131,7 +131,7 @@ let rec make_hyps atom_env gls lenv = function
   | LocalAssum (id,typ)::rest ->
       let hrec=
 	make_hyps atom_env gls (typ::lenv) rest in
-	if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv ||
+        if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv ||
 	  (Retyping.get_sort_family_of
 	     (pf_env gls) (Tacmach.project gls) typ != InProp)
 	then
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 4109e9cf38..9fea3ddcda 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -194,12 +194,12 @@ let exec_tactic env evd n f args =
   in
   let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
   let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
-  (** Build the getter *)
+  (* Build the getter *)
   let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
   let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
   let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in
   let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
-  (** Evaluate the whole result *)
+  (* Evaluate the whole result *)
   let gl = dummy_goal env evd in
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
   let evd = Evd.minimize_universes (Refiner.project gls) in
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index bb8a0faf2e..11e282e4f5 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -104,6 +104,7 @@ type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats
 
 
 type ssrfwdid = Id.t
+
 (** Binders (for fwd tactics) *)
 type 'term ssrbind =
   | Bvar of Name.t
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index efc4a2c743..cd9af84ed9 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -263,7 +263,7 @@ let of_ftactic ftac gl =
   let tac = Proofview.V82.of_tactic tac in
   let { sigma = sigma } = tac gl in
   let ans = match !r with
-  | None -> assert false (** If the tactic failed we should not reach this point *)
+  | None -> assert false (* If the tactic failed we should not reach this point *)
   | Some ans -> ans
   in
   (sigma, ans)
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 0553260472..18b4aeab1e 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -86,9 +86,9 @@ end (* }}} *************************************************************** *)
 
 open State
 
-(** [=> *] ****************************************************************)
-(** [nb_assums] returns the number of dependent premises *)
-(** Warning: unlike [nb_deps_assums], it does not perform reduction *)
+(***[=> *] ****************************************************************)
+(** [nb_assums] returns the number of dependent premises
+    Warning: unlike [nb_deps_assums], it does not perform reduction *)
 let rec nb_assums cur env sigma t =
   match EConstr.kind sigma t with
   | Prod(name,ty,body) ->
@@ -148,7 +148,7 @@ let tac_case t =
       Ssrelim.ssrscasetac t
 end
 
-(** [=> [: id]] ************************************************************)
+(***[=> [: id]] ************************************************************)
 [@@@ocaml.warning "-3"]
 let mk_abstract_id =
   let open Coqlib in
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 4ed75cdbe4..191a4e9a20 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat =
     Pattern.PApp (fp, args') in
   let hr, na = splay_search_pattern 0 hpat in
   let dc, ht =
-    let hr, _ = Typeops.type_of_global_in_context env hr (** FIXME *) in
+    let hr, _ = Typeops.type_of_global_in_context env hr (* FIXME *) in
     Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
   let np = List.length dc in
   if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 6497b6ff98..efd65ade15 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -122,6 +122,7 @@ let add_genarg tag pr =
 
 (** Constructors for cast type *)
 let dC t = CastConv t
+
 (** Constructors for constr_expr *)
 let isCVar   = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false
 let destCVar = function
@@ -139,6 +140,7 @@ let mkCLambda ?loc name ty t = CAst.make ?loc @@
 let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((CAst.make ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
+
 (** Constructors for rawconstr *)
 let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None)
 let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
@@ -925,7 +927,7 @@ let of_ftactic ftac gl =
   let tac = Proofview.V82.of_tactic tac in
   let { sigma = sigma } = tac gl in
   let ans = match !r with
-  | None -> assert false (** If the tactic failed we should not reach this point *)
+  | None -> assert false (* If the tactic failed we should not reach this point *)
   | Some ans -> ans
   in
   (sigma, ans)
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 8672c55767..f0bb6f58a6 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -194,6 +194,7 @@ val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> c
 
 (** [do_once r f] calls [f] and updates the ref only once *)
 val do_once : 'a option ref -> (unit -> 'a) -> unit
+
 (** [assert_done r] return the content of r. @raise Anomaly is r is [None] *)
 val assert_done : 'a option ref -> 'a
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fe67f5767b..62c27297f3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1015,9 +1015,9 @@ let add_assert_false_case pb tomatch =
 let adjust_impossible_cases sigma pb pred tomatch submat =
   match submat with
   | [] ->
-    (** FIXME: This breaks if using evar-insensitive primitives. In particular,
-        this means that the Evd.define below may redefine an already defined
-        evar. See e.g. first definition of test for bug #3388. *)
+    (* FIXME: This breaks if using evar-insensitive primitives. In particular,
+       this means that the Evd.define below may redefine an already defined
+       evar. See e.g. first definition of test for bug #3388. *)
     let pred = EConstr.Unsafe.to_constr pred in
     begin match Constr.kind pred with
     | Evar (evk,_) when snd (evar_source evk sigma) == Evar_kinds.ImpossibleCase ->
@@ -1684,8 +1684,8 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
      convertible subterms of the substitution *)
   let evdref = ref sigma in
   let rec aux (k,env,subst as x) t =
-    (** Use a reference because the [map_constr_with_full_binders] does not
-        allow threading a state. *)
+    (* Use a reference because the [map_constr_with_full_binders] does not
+       allow threading a state. *)
     let sigma = !evdref in
     match EConstr.kind sigma t with
     | Rel n when is_local_def (lookup_rel n !!env) -> t
@@ -2021,7 +2021,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 
 let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
   let refresh_tycon sigma t =
-    (** If we put the typing constraint in the term, it has to be
+    (* If we put the typing constraint in the term, it has to be
        refreshed to preserve the invariant that no algebraic universe
        can appear in the term.  *)
     refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index d7118efd7a..032e4bbf85 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -96,8 +96,8 @@ let rec build_lambda sigma vars ctx m = match vars with
   | (_, id, t) :: suf ->
      (Name id, t, suf)
   in
-  (** Check that the abstraction is legal by generating a transitive closure of
-      its dependencies. *)
+  (* Check that the abstraction is legal by generating a transitive closure of
+     its dependencies. *)
   let is_nondep t clear = match clear with
   | [] -> true
   | _ ->
@@ -106,12 +106,12 @@ let rec build_lambda sigma vars ctx m = match vars with
     List.for_all_i check 1 clear
   in
   let fold (_, _, t) clear = is_nondep t clear :: clear in
-  (** Produce a list of booleans: true iff we keep the hypothesis *)
+  (* Produce a list of booleans: true iff we keep the hypothesis *)
   let clear = List.fold_right fold pre [false] in
   let clear = List.drop_last clear in
-  (** If the conclusion depends on a variable we cleared, failure *)
+  (* If the conclusion depends on a variable we cleared, failure *)
   let () = if not (is_nondep m clear) then raise PatternMatchingFailure in
-  (** Create the abstracted term *)
+  (* Create the abstracted term *)
   let fold (k, accu) keep =
     if keep then
       let k = succ k in
@@ -121,10 +121,10 @@ let rec build_lambda sigma vars ctx m = match vars with
   let keep, shift = List.fold_left fold (0, []) clear in
   let shift = List.rev shift in
   let map = function
-  | None -> mkProp (** dummy term *)
+  | None -> mkProp (* dummy term *)
   | Some i -> mkRel (i + 1)
   in
-  (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *)
+  (* [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *)
   let subst =
     List.map map shift @
     mkRel 1 ::
@@ -143,12 +143,12 @@ let rec build_lambda sigma vars ctx m = match vars with
     if i > n then i - n + keep
     else match List.nth shift (i - 1) with
     | None ->
-      (** We cleared a variable that we wanted to abstract! *)
+      (* We cleared a variable that we wanted to abstract! *)
       raise PatternMatchingFailure
     | Some k -> k
   in
   let vars = List.map map vars in
-  (** Create the abstraction *)
+  (* Create the abstraction *)
   let m = mkLambda (na, Vars.lift keep t, m) in
   build_lambda sigma vars (pre @ suf) m
 
@@ -377,8 +377,8 @@ let matches_core env sigma allow_bound_rels
           let () = match ci1.cip_ind with
           | None -> ()
           | Some ind1 ->
-            (** ppedrot: Something spooky going here. The comparison used to be
-                the generic one, so I may have broken something. *)
+            (* ppedrot: Something spooky going here. The comparison used to be
+               the generic one, so I may have broken something. *)
             if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure
           in
           let () =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ce7c7c8702..09b3cf167f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -703,7 +703,7 @@ and detype_r d flags avoid env sigma t =
 		[detype d flags avoid env sigma c])
       else 
 	if print_primproj_compatibility () && Projection.unfolded p then
-	  (** Print the compatibility match version *)
+          (* Print the compatibility match version *)
 	  let c' = 
 	    try 
               let ind = Projection.inductive p in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6c268de3b3..e6e1530e36 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1311,10 +1311,10 @@ let max_undefined_with_candidates evd =
   | None -> ()
   | Some l -> raise (MaxUndefined (evk, evi, l))
   in
-  (** [fold_right] traverses the undefined map in decreasing order of indices.
-  The evar with candidates of maximum index is thus the first evar with
-  candidates found by a [fold_right] traversal. This has a significant impact on
-  performance. *)
+  (* [fold_right] traverses the undefined map in decreasing order of
+     indices.  The evar with candidates of maximum index is thus the
+     first evar with candidates found by a [fold_right]
+     traversal. This has a significant impact on performance. *)
   try
     let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in
     None
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4692fe0057..4c4a236620 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -80,7 +80,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
        if v' == v then t else mkProd (na, u, v')
     | _ -> t
   in
-  (** Refresh the types of evars under template polymorphic references *)
+  (* Refresh the types of evars under template polymorphic references *)
   let rec refresh_term_evars ~onevars ~top t =
     match EConstr.kind !evdref t with
     | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f ->
@@ -1385,7 +1385,7 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
 let occur_evar_upto_types sigma n c =
   let c = EConstr.Unsafe.to_constr c in
   let seen = ref Evar.Set.empty in
-  (** FIXME: Is that supposed to be evar-insensitive? *)
+  (* FIXME: Is that supposed to be evar-insensitive? *)
   let rec occur_rec c = match Constr.kind c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
     | Evar (sp,args as e) ->
@@ -1581,7 +1581,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
       Id.Set.subset (collect_vars evd rhs) !names 
   in
   let body =
-    if fast rhs then nf_evar evd rhs (** FIXME? *)
+    if fast rhs then nf_evar evd rhs (* FIXME? *)
     else
       let t' = imitate (env,0) rhs in
 	if !progress then
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 9b2da0b084..e14766f370 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -148,7 +148,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     Array.equal f c1 c2 && Array.equal f t1 t2
   | GSort s1, GSort s2 -> glob_sort_eq s1 s2
   | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
-    Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
+    Option.equal (==) gn1 gn2 (* Only thing sensible *) &&
     Namegen.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index c6fdb0ec14..c405fcfc72 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -106,6 +106,7 @@ and 'a tomatch_tuples_g = 'a tomatch_tuple_g list
 and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.t
 (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables
     of [t] are members of [il]. *)
+
 and 'a cases_clauses_g = 'a cases_clause_g list
 
 type glob_constr = [ `any ] glob_constr_g
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 10d8451947..ff552c7caf 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -469,9 +469,9 @@ let compute_projections env (kn, i as ind) =
   let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
   let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
   let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
-  (** We build a substitution smashing the lets in the record parameters so
-      that typechecking projections requires just a substitution and not
-      matching with a parameter context. *)
+  (* We build a substitution smashing the lets in the record parameters so
+     that typechecking projections requires just a substitution and not
+     matching with a parameter context. *)
   let indty =
     (* [ty] = [Ind inst] is typed in context [params] *)
     let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
@@ -748,7 +748,7 @@ let type_of_projection_knowing_arg env sigma p c ty =
 let control_only_guard env sigma c =
   let c = Evarutil.nf_evar sigma c in
   let check_fix_cofix e c =
-    (** [c] has already been normalized upfront *)
+    (* [c] has already been normalized upfront *)
     let c = EConstr.Unsafe.to_constr c in
     match kind c with
     | CoFix (_,(_,_,_) as cofix) ->
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 022c383f60..dc2663c1ca 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -406,14 +406,15 @@ and nf_evar env sigma evk args =
     mkEvar (evk, [||]), ty
   end
   else
-    (** Let-bound arguments are present in the evar arguments but not in the
-        type, so we turn the let into a product. *)
+    (* Let-bound arguments are present in the evar arguments but not
+       in the type, so we turn the let into a product. *)
     let hyps = Context.Named.drop_bodies hyps in
     let fold accu d = Term.mkNamedProd_or_LetIn d accu in
     let t = List.fold_left fold ty hyps in
     let ty, args = nf_args env sigma args t in
-    (** nf_args takes arguments in the reverse order but produces them in the
-        correct one, so we have to reverse them again for the evar node *)
+    (* nf_args takes arguments in the reverse order but produces them
+       in the correct one, so we have to reverse them again for the
+       evar node *)
     mkEvar (evk, Array.rev_of_list args), ty
 
 let evars_of_evar_map sigma =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3c1c470053..a3ab250784 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -256,7 +256,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *)
+          (* FIXME: Stupid workaround to pattern_of_constr being evar sensitive *)
 	  let c = Evarutil.nf_evar sigma c in
 	  pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
 	with Not_found (* List.index failed *) ->
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 054f0c76a9..51103ca194 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -38,12 +38,15 @@ type subterm_unification_error = bool * position_reporting * position_reporting
 type type_error = (constr, types) ptype_error
 
 type pretype_error =
-  (** Old Case *)
   | CantFindCaseType of constr
-  (** Type inference unification *)
+  (** Old Case *)
+
   | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
-  (** Tactic Unification *)
+  (** Type inference unification *)
+
   | UnifOccurCheck of Evar.t * constr
+  (** Tactic Unification *)
+
   | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option
   | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2be0f73ea4..ace2868255 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -212,7 +212,7 @@ type frozen =
 
 let frozen_and_pending_holes (sigma, sigma') =
   let undefined0 = Option.cata Evd.undefined_map Evar.Map.empty sigma in
-  (** Fast path when the undefined evars where not modified *)
+  (* Fast path when the undefined evars where not modified *)
   if undefined0 == Evd.undefined_map sigma' then
     FrozenId undefined0
   else
@@ -579,7 +579,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         sigma ctxtv vdef in
       let sigma = Typing.check_type_fixpoint ?loc !!env sigma names ftys vdefj in
       let nf c = nf_evar sigma c in
-      let ftys = Array.map nf ftys in (** FIXME *)
+      let ftys = Array.map nf ftys in (* FIXME *)
       let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in
       let fixj = match fixkind with
 	| GFix (vn,i) ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index fe9b69dbbc..0c4a2e2a99 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -374,7 +374,7 @@ let decompose_projection sigma c args =
   match EConstr.kind sigma c with
   | Const (c, u) ->
      let n = find_projection_nparams (ConstRef c) in
-     (** Check if there is some canonical projection attached to this structure *)
+     (* Check if there is some canonical projection attached to this structure *)
      let _ = GlobRef.Map.find (ConstRef c) !object_table in
      let arg = Stack.nth args n in
      arg
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a57ee6e292..f8e8fa9eb9 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -203,6 +203,7 @@ end
 (** Machinery about stack of unfolded constants *)
 module Cst_stack = struct
   open EConstr
+
 (** constant * params * args
 
 - constant applied to params = term in head applied to args
@@ -1342,7 +1343,7 @@ let sigma_univ_state =
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=TransparentState.full) env sigma x y =
-  (** FIXME *)
+  (* FIXME *)
   try
       let ans = match pb with
       | Reduction.CUMUL ->
@@ -1632,7 +1633,7 @@ let meta_reducible_instance evd b =
   in
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
-    let u = whd_betaiota Evd.empty u (** FIXME *) in
+    let u = whd_betaiota Evd.empty u (* FIXME *) in
     match EConstr.kind evd u with
     | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
 	let m = destMeta evd (strip_outer_cast evd c) in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 088e898a99..a1fd610676 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -77,7 +77,9 @@ module Stack : sig
   | Case of case_info * 'a * 'a array * Cst_stack.t
   | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
-  | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
+  | Cst of cst_member
+           * int (* current foccussed arg *)
+           * int list (* remaining args *)
     * 'a t * Cst_stack.t
   and 'a t = 'a member list
 
@@ -93,6 +95,7 @@ module Stack : sig
   val compare_shape : 'a t -> 'a t -> bool
 
   exception IncompatibleFold2
+
   (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
       @return the result and the lifts to apply on the terms
       @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *)
@@ -104,6 +107,7 @@ module Stack : sig
   (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not
       start by App *)
   val strip_app : 'a t -> 'a t * 'a t
+
   (** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index d9df8c8cf8..2e7176a6b3 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -250,7 +250,7 @@ let invert_name labs l na0 env sigma ref = function
 		    let labs',ccl = decompose_lam sigma c in
 		    let _, l' = whd_betalet_stack sigma ccl in
 		    let labs' = List.map snd labs' in
-		    (** ppedrot: there used to be generic equality on terms here *)
+                    (* ppedrot: there used to be generic equality on terms here *)
                     let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in
 		    if List.equal eq_constr labs' labs &&
                        List.equal eq_constr l l' then Some (minfxargs,ref)
@@ -450,7 +450,7 @@ let substl_checking_arity env subst sigma c =
      the other ones are replaced by the function symbol *)
   let rec nf_fix c = match EConstr.kind sigma c with
   | Evar (i,[|fx;f|]) when Evar.Map.mem i minargs ->
-    (** FIXME: find a less hackish way of doing this *)
+    (* FIXME: find a less hackish way of doing this *)
     begin match EConstr.kind sigma' c with
     | Evar _ -> f
     | c -> EConstr.of_kind c
@@ -943,7 +943,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
 	  | _ -> false) ->
         let npars = Projection.npars p in
           if List.length stack <= npars then
-	    (** Do not show the eta-expanded form *)
+            (* Do not show the eta-expanded form *)
 	    s'
 	  else redrec (applist (c, stack))
       | _ -> redrec (applist(c, stack)))
@@ -993,7 +993,7 @@ let e_contextually byhead (occs,c) f = begin fun env sigma t ->
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref 1 in
-  (** FIXME: we do suspicious things with this evarmap *)
+  (* FIXME: we do suspicious things with this evarmap *)
   let evd = ref sigma in
   let rec traverse nested (env,c as envc) t =
     if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index d00195678b..f8aedf88c2 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -25,33 +25,33 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 
 (** This module defines type-classes *)
 type typeclass = {
+  cl_univs : Univ.AUContext.t;
   (** The toplevel universe quantification in which the typeclass lives. In
       particular, [cl_props] and [cl_context] are quantified over it. *)
-  cl_univs : Univ.AUContext.t;
 
+  cl_impl : GlobRef.t;
   (** The class implementation: a record parameterized by the context with defs in it or a definition if
      the class is a singleton. This acts as the class' global identifier. *)
-  cl_impl : GlobRef.t;
 
+  cl_context : GlobRef.t option list * Constr.rel_context;
   (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
       The global reference gives a direct link to the class itself. *)
-  cl_context : GlobRef.t option list * Constr.rel_context;
 
-  (** Context of definitions and properties on defs, will not be shared *)
   cl_props : Constr.rel_context;
+  (** Context of definitions and properties on defs, will not be shared *)
 
+  cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list;
   (** The methods implementations of the typeclass as projections. 
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list;
 
-  (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
+  (** Whether we use matching or full unification during resolution *)
 
+  cl_unique : bool;
   (** Whether we can assume that instances are unique, which allows 
       no backtracking and sharing of resolution. *)
-  cl_unique : bool; 
 }
 
 type instance
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 366af0772f..79f2941554 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -36,8 +36,8 @@ val meta_type : evar_map -> metavariable -> types
 (** Solve existential variables using typing *)
 val solve_evars : env -> evar_map -> constr -> evar_map * constr
 
-(** Raise an error message if incorrect elimination for this inductive *)
-(** (first constr is term to match, second is return predicate) *)
+(** Raise an error message if incorrect elimination for this inductive
+    (first constr is term to match, second is return predicate) *)
 val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
   unit
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 094fcd923e..f0cd5c5f6a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -76,8 +76,8 @@ let unsafe_occur_meta_or_existential c =
 
 
 let occur_meta_or_undefined_evar evd c =
-  (** This is performance-critical. Using the evar-insensitive API changes the
-      resulting heuristic. *)
+  (* This is performance-critical. Using the evar-insensitive API changes the
+     resulting heuristic. *)
   let c = EConstr.Unsafe.to_constr c in
   let rec occrec c = match Constr.kind c with
     | Meta _ -> raise Occur
@@ -134,7 +134,7 @@ let abstract_list_all env evd typ c l =
     | UserError _ ->
         error_cannot_find_well_typed_abstraction env evd p l None
     | Type_errors.TypeError (env',x) ->
-        (** FIXME: plug back the typing information *)
+        (* FIXME: plug back the typing information *)
         error_cannot_find_well_typed_abstraction env evd p l None
     | Pretype_errors.PretypeError (env',evd,TypingError x) ->
         error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
@@ -154,11 +154,9 @@ let abstract_list_all_with_dependencies env evd typ c l =
   if b then
     let p = nf_evar evd ev in
       evd, p
-  else error_cannot_find_well_typed_abstraction env evd 
+  else error_cannot_find_well_typed_abstraction env evd
     c l None
 
-(**)
-
 (* A refinement of [conv_pb]: the integers tells how many arguments
    were applied in the context of the conversion problem; if the number
    is non zero, steps of eta-expansion will be allowed
@@ -598,8 +596,9 @@ let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
 
 
 let subst_defined_metas_evars sigma (bl,el) c =
-  (** This seems to be performance-critical, and using the evar-insensitive
-      primitives blow up the time passed in this function. *)
+  (* This seems to be performance-critical, and using the
+     evar-insensitive primitives blow up the time passed in this
+     function. *)
   let c = EConstr.Unsafe.to_constr c in
   let rec substrec c = match Constr.kind c with
     | Meta i ->
@@ -656,7 +655,7 @@ let is_eta_constructor_app env sigma ts f l1 term =
       | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite &&
           let (_, projs, _) = info.(i) in
           Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
-	(** Check that the other term is neutral *)
+        (* Check that the other term is neutral *)
 	is_neutral env sigma ts term
       | _ -> false)
   | _ -> false
@@ -783,7 +782,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN
 	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
 
-	(** Fast path for projections. *)
+        (* Fast path for projections. *)
 	| Proj (p1,c1), Proj (p2,c2) when Constant.equal
 	    (Projection.constant p1) (Projection.constant p2) ->
 	  (try unify_same_proj curenvnb cv_pb {opt with at_top = true}
@@ -908,7 +907,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       	match EConstr.kind sigma c with
       	| Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' ->
       	  (try destApp sigma (Retyping.expand_projection curenv sigma p t (Array.to_list l))
-      	   with RetypeError _ -> (** Unification can be called on ill-typed terms, due
+           with RetypeError _ -> (* Unification can be called on ill-typed terms, due
       				     to FO and eta in particular, fail gracefully in that case *)
       	     (c, l))
       	| _ -> (c, l)
@@ -1604,7 +1603,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     with
     | PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
         raise (NotUnifiable (Some (c1,c2,e)))
-    (** MS: This is pretty bad, it catches Not_found for example *)
+    (* MS: This is pretty bad, it catches Not_found for example *)
     | e when CErrors.noncritical e -> raise (NotUnifiable None) in
   let merge_fun c1 c2 =
     match c1, c2 with
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c30c4f0932..113aac25da 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -207,10 +207,10 @@ and nf_evar env sigma evk stk =
     nf_stk env sigma (mkEvar (evk, [||])) concl stk
   else match stk with
   | Zapp args :: stk ->
-    (** We assume that there is no consecutive Zapp nodes in a VM stack. Is that
-        really an invariant? *)
-    (** Let-bound arguments are present in the evar arguments but not in the
-        type, so we turn the let into a product. *)
+    (* We assume that there is no consecutive Zapp nodes in a VM stack. Is that
+       really an invariant? *)
+    (* Let-bound arguments are present in the evar arguments but not in the
+       type, so we turn the let into a product. *)
     let hyps = Context.Named.drop_bodies hyps in
     let fold accu d = Term.mkNamedProd_or_LetIn d accu in
     let t = List.fold_left fold concl hyps in
@@ -388,7 +388,7 @@ and nf_cofix env sigma cf =
 let cbv_vm env sigma c t  =
   if Termops.occur_meta sigma c then
     CErrors.user_err Pp.(str "vm_compute does not support metas.");
-  (** This evar-normalizes terms beforehand *)
+  (* This evar-normalizes terms beforehand *)
   let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
   let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
   let v = Csymtable.val_of_constr env c in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f9f4d7f7f8..8f7e4470f9 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -427,7 +427,7 @@ let locate_modtype qid =
   let all = Nametab.locate_extended_all_modtype qid in
   let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in
   let modtypes = List.map map all in
-  (** Don't forget the opened module types: they are not part of the same name tab. *)
+  (* Don't forget the opened module types: they are not part of the same name tab. *)
   let all = Nametab.locate_extended_all_dir qid in
   let map dir = let open Nametab.GlobDirRef in match dir with
   | DirOpenModtype _ -> Some (Dir dir, qid)
diff --git a/printing/printer.ml b/printing/printer.ml
index 2bbda279bd..83f1f8d8e9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -605,12 +605,12 @@ let print_evar_constraints gl sigma =
     let t1 = Evarutil.nf_evar sigma t1
     and t2 = Evarutil.nf_evar sigma t2 in
     let env =
-      (** We currently allow evar instances to refer to anonymous de Bruijn
-          indices, so we protect the error printing code in this case by giving
-          names to every de Bruijn variable in the rel_context of the conversion
-          problem. MS: we should rather stop depending on anonymous variables, they
-          can be used to indicate independency. Also, this depends on a strategy for 
-          naming/renaming *)
+      (* We currently allow evar instances to refer to anonymous de Bruijn
+         indices, so we protect the error printing code in this case by giving
+         names to every de Bruijn variable in the rel_context of the conversion
+         problem. MS: we should rather stop depending on anonymous variables, they
+         can be used to indicate independency. Also, this depends on a strategy for
+         naming/renaming *)
       Namegen.make_all_name_different env sigma in
     str" " ++
       hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++
@@ -686,7 +686,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
     | None -> GoalMap.empty
   in
 
-  (** Printing functions for the extra informations. *)
+  (* Printing functions for the extra informations. *)
   let rec print_stack a = function
     | [] -> Pp.int a
     | b::l -> Pp.int a ++ str"-" ++ print_stack b l
@@ -753,7 +753,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
     | None -> ()
   in
 
-  (** Main function *)
+  (* Main function *)
   match goals with
   | [] ->
       begin
diff --git a/printing/printer.mli b/printing/printer.mli
index b0232ec4ac..357f30d1f4 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -112,6 +112,7 @@ val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t
 
 
 (** Contexts *)
+
 (** Display compact contexts of goals (simple hyps on the same line) *)
 val set_compact_context : bool -> unit
 val get_compact_context : unit -> bool
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index ce9ee5ae6f..1ebde3d572 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -12,6 +12,7 @@
 
 (** Controls whether to show diffs.  Takes values "on", "off", "removed" *)
 val write_diffs_option : string -> unit
+
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index b7ccd647b5..1f1bdf4da7 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -601,17 +601,17 @@ let make_evar_clause env sigma ?len t =
   | None -> -1
   | Some n -> assert (0 <= n); n
   in
-  (** FIXME: do the renaming online *)
+  (* FIXME: do the renaming online *)
   let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
   let rec clrec (sigma, holes) inst n t =
     if n = 0 then (sigma, holes, t)
     else match EConstr.kind sigma t with
     | Cast (t, _, _) -> clrec (sigma, holes) inst n t
     | Prod (na, t1, t2) ->
-      (** Share the evar instances as we are living in the same context *)
+      (* Share the evar instances as we are living in the same context *)
       let inst, ctx, args, subst = match inst with
       | None ->
-        (** Dummy type *)
+        (* Dummy type *)
         let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in
         Some (ctx, args, subst), ctx, args, subst
       | Some (ctx, args, subst) -> inst, ctx, args, subst
@@ -688,7 +688,7 @@ let solve_evar_clause env sigma hyp_only clause = function
   let open EConstr in
   let fold holes h =
     if h.hole_deps then
-      (** Some subsequent term uses the hole *)
+      (* Some subsequent term uses the hole *)
       let (ev, _) = destEvar sigma h.hole_evar in
       let is_dep hole = occur_evar sigma ev hole.hole_type in
       let in_hyp = List.exists is_dep holes in
@@ -697,7 +697,7 @@ let solve_evar_clause env sigma hyp_only clause = function
       let h = { h with hole_deps = dep } in
       h :: holes
     else
-      (** The hole does not occur anywhere *)
+      (* The hole does not occur anywhere *)
       h :: holes
   in
   let holes = List.fold_left fold [] (List.rev clause.cl_holes) in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 4720328893..c36b0fa337 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -61,9 +61,9 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
   clenv_pose_metas_as_evars clenv dep_mvs
 
 let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
-  (** ppedrot: a Goal.enter here breaks things, because the tactic below may
-      solve goals by side effects, while the compatibility layer keeps those
-      useless goals. That deserves a FIXME. *)
+  (* ppedrot: a Goal.enter here breaks things, because the tactic below may
+     solve goals by side effects, while the compatibility layer keeps those
+     useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
   let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 15ba0a704f..456ab879eb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -373,8 +373,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	check_typability env sigma ty;
         let sigma = check_conv_leq_goal env sigma trm ty conclty in
 	let res = mk_refgoals sigma goal goalacc ty t in
-	(** we keep the casts (in particular VMcast and NATIVEcast) except
-	    when they are annotating metas *)
+        (* we keep the casts (in particular VMcast and NATIVEcast) except
+           when they are annotating metas *)
 	if isMeta t then begin
 	  assert (k != VMcast && k != NATIVEcast);
 	  res
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 886a62cb89..acf5510aa0 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -167,23 +167,23 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   cb, status, univs
 
 let refine_by_tactic env sigma ty tac =
-  (** Save the initial side-effects to restore them afterwards. We set the
-      current set of side-effects to be empty so that we can retrieve the
-      ones created during the tactic invocation easily. *)
+  (* Save the initial side-effects to restore them afterwards. We set the
+     current set of side-effects to be empty so that we can retrieve the
+     ones created during the tactic invocation easily. *)
   let eff = Evd.eval_side_effects sigma in
   let sigma = Evd.drop_side_effects sigma in
-  (** Save the existing goals *)
+  (* Save the existing goals *)
   let prev_future_goals = save_future_goals sigma in
-  (** Start a proof *)
+  (* Start a proof *)
   let prf = Proof.start sigma [env, ty] in
   let (prf, _) =
     try Proof.run_tactic env tac prf
     with Logic_monad.TacticFailure e as src ->
-      (** Catch the inner error of the monad tactic *)
+      (* Catch the inner error of the monad tactic *)
       let (_, info) = CErrors.push src in
       iraise (e, info)
   in
-  (** Plug back the retrieved sigma *)
+  (* Plug back the retrieved sigma *)
   let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in
   assert (stack = []);
   let ans = match Proof.initial_goals prf with
@@ -191,26 +191,26 @@ let refine_by_tactic env sigma ty tac =
   | _ -> assert false
   in
   let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
-  (** [neff] contains the freshly generated side-effects *)
+  (* [neff] contains the freshly generated side-effects *)
   let neff = Evd.eval_side_effects sigma in
-  (** Reset the old side-effects *)
+  (* Reset the old side-effects *)
   let sigma = Evd.drop_side_effects sigma in
   let sigma = Evd.emit_side_effects eff sigma in
-  (** Restore former goals *)
+  (* Restore former goals *)
   let sigma = restore_future_goals sigma prev_future_goals in
-  (** Push remaining goals as future_goals which is the only way we
-      have to inform the caller that there are goals to collect while
-      not being encapsulated in the monad *)
-  (** Goals produced by tactic "shelve" *)
+  (* Push remaining goals as future_goals which is the only way we
+     have to inform the caller that there are goals to collect while
+     not being encapsulated in the monad *)
+  (* Goals produced by tactic "shelve" *)
   let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
-  (** Goals produced by tactic "give_up" *)
+  (* Goals produced by tactic "give_up" *)
   let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
-  (** Other goals *)
+  (* Other goals *)
   let sigma = List.fold_right Evd.declare_future_goal goals sigma in
-  (** Get rid of the fresh side-effects by internalizing them in the term
-      itself. Note that this is unsound, because the tactic may have solved
-      other goals that were already present during its invocation, so that
-      those goals rely on effects that are not present anymore. Hopefully,
-      this hack will work in most cases. *)
+  (* Get rid of the fresh side-effects by internalizing them in the term
+     itself. Note that this is unsound, because the tactic may have solved
+     other goals that were already present during its invocation, so that
+     those goals rely on effects that are not present anymore. Hopefully,
+     this hack will work in most cases. *)
   let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
   ans, sigma
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 67e19df0e7..76a1e61ad2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -422,9 +422,9 @@ let return_proof ?(allow_partial=false) () =
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in
   let eff = Evd.eval_side_effects evd in
-  (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-      side-effects... This may explain why one need to uniquize side-effects
-      thereafter... *)
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
   let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
     proofs, Evd.evar_universe_context evd
  end else
@@ -432,9 +432,9 @@ let return_proof ?(allow_partial=false) () =
   let evd = Proof.return ~pid proof in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.minimize_universes evd in
-  (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-      side-effects... This may explain why one need to uniquize side-effects
-      thereafter... *)
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
   let proofs =
     List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 540a8bb420..d812a8cad7 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -27,7 +27,7 @@ let extract_prefix env info =
 
 let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
-  (** Typecheck the hypotheses. *)
+  (* Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
     let t = NamedDecl.get_type decl in
     let sigma, _ = Typing.sort_of env sigma t in
@@ -40,7 +40,7 @@ let typecheck_evar ev env sigma =
   let (common, changed) = extract_prefix env info in
   let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
-  (** Typecheck the conclusion *)
+  (* Typecheck the conclusion *)
   let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
   sigma
 
@@ -60,39 +60,39 @@ let generic_refine ~typecheck f gl =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   let state = Proofview.Goal.state gl in
-  (** Save the [future_goals] state to restore them after the
-      refinement. *)
+  (* Save the [future_goals] state to restore them after the
+     refinement. *)
   let prev_future_goals = Evd.save_future_goals sigma in
-  (** Create the refinement term *)
+  (* Create the refinement term *)
   Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
   f >>= fun (v, c) ->
   Proofview.tclEVARMAP >>= fun sigma ->
   Proofview.V82.wrap_exceptions begin fun () ->
   let evs = Evd.save_future_goals sigma in
-  (** Redo the effects in sigma in the monad's env *)
+  (* Redo the effects in sigma in the monad's env *)
   let privates_csts = Evd.eval_side_effects sigma in
   let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
   let env = add_side_effects env sideff in
-  (** Check that the introduced evars are well-typed *)
+  (* Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
-  (** Check that the refined term is typesafe *)
+  (* Check that the refined term is typesafe *)
   let sigma = if typecheck then Typing.check env sigma c concl else sigma in
-  (** Check that the goal itself does not appear in the refined term *)
+  (* Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
     if not (Evarutil.occur_evar_upto sigma self c) then ()
     else Pretype_errors.error_occur_check env sigma self c
   in
-  (** Restore the [future goals] state. *)
+  (* Restore the [future goals] state. *)
   let sigma = Evd.restore_future_goals sigma prev_future_goals in
-  (** Select the goals *)
+  (* Select the goals *)
   let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
   let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
-  (** Proceed to the refinement *)
+  (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
-    (** Nothing to do, the goal has been solved by side-effect *)
+    (* Nothing to do, the goal has been solved by side-effect *)
     sigma
   | Some self ->
     match evkmain with
@@ -104,7 +104,7 @@ let generic_refine ~typecheck f gl =
         | None -> sigma
         | Some id -> Evd.rename evk id sigma
   in
-  (** Mark goals *)
+  (* Mark goals *)
   let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
   let trace () = Pp.(hov 2 (str"simple refine"++spc()++
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 64d7630d55..a5f691babb 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -133,7 +133,7 @@ module New = struct
     f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
   let pf_global id gl =
-    (** We only check for the existence of an [id] in [hyps] *)
+    (* We only check for the existence of an [id] in [hyps] *)
     let hyps = Proofview.Goal.hyps gl in
     Constrintern.construct_reference hyps id
 
@@ -149,12 +149,12 @@ module New = struct
   let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
 
   let pf_ids_of_hyps gl =
-    (** We only get the identifiers in [hyps] *)
+    (* We only get the identifiers in [hyps] *)
     let hyps = Proofview.Goal.hyps gl in
     ids_of_named_context hyps
 
   let pf_ids_set_of_hyps gl =
-    (** We only get the identifiers in [hyps] *)
+    (* We only get the identifiers in [hyps] *)
     let env = Proofview.Goal.env gl in
     Environ.ids_of_named_context_val (Environ.named_context_val env)
 
@@ -186,7 +186,7 @@ module New = struct
     List.hd hyps
 
   let pf_nf_concl (gl : Proofview.Goal.t) =
-    (** We normalize the conclusion just after *)
+    (* We normalize the conclusion just after *)
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
     nf_evar sigma concl
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index 6e6827c73f..067ea5df0c 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -70,6 +70,7 @@ module type Task = sig
 
   (** UID of the task kind, for -toploop *)
   val name : string ref
+
   (** Extra arguments of the task kind, for -toploop *)
   val extra_env : unit -> string array
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 3444229735..e835bdcb1e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1087,7 +1087,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
       (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
     else
       match cmd with
-      | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *)
+      | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *)
       | _ ->
         stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
         try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr)
@@ -1750,7 +1750,7 @@ end = struct (* {{{ *)
         let uc =
           Option.get
             (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
-        (** We only manipulate monomorphic terms here. *)
+        (* We only manipulate monomorphic terms here. *)
         let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
         let pr =
           Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 3c262de910..3a687a6b41 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -76,7 +76,7 @@ let shrink_entry sign const =
   | None -> assert false
   | Some t -> t
   in
-  (** The body has been forced by the call to [build_constant_by_tactic] *)
+  (* The body has been forced by the call to [build_constant_by_tactic] *)
   let () = assert (Future.is_over const.const_entry_body) in
   let ((body, uctx), eff) = Future.force const.const_entry_body in
   let (body, typ, ctx) = decompose (List.length sign) body typ [] in
@@ -140,18 +140,18 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in
   let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
   let cst () =
-    (** do not compute the implicit arguments, it may be costly *)
+    (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
-    (** ppedrot: seems legit to have abstracted subproofs as local*)
+    (* ppedrot: seems legit to have abstracted subproofs as local*)
     Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
   in
   let cst = Impargs.with_implicit_protection cst () in
   let inst = match const.Entries.const_entry_universes with
   | Entries.Monomorphic_const_entry _ -> EInstance.empty
   | Entries.Polymorphic_const_entry (_, ctx) ->
-    (** We mimick what the kernel does, that is ensuring that no additional
-        constraints appear in the body of polymorphic constants. Ideally this
-        should be enforced statically. *)
+    (* We mimick what the kernel does, that is ensuring that no additional
+       constraints appear in the body of polymorphic constants. Ideally this
+       should be enforced statically. *)
     let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
     let () = assert (Univ.ContextSet.is_empty body_uctx) in
     EInstance.make (Univ.UContext.instance ctx)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 441fb68acc..c030c77d4d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -70,19 +70,19 @@ let auto_unif_flags =
 (* Try unification with the precompiled clause, then use registered Apply *)
 
 let connect_hint_clenv poly (c, _, ctx) clenv gl =
-  (** [clenv] has been generated by a hint-making function, so the only relevant
-      data in its evarmap is the set of metas. The [evar_reset_evd] function
-      below just replaces the metas of sigma by those coming from the clenv. *)
+  (* [clenv] has been generated by a hint-making function, so the only relevant
+     data in its evarmap is the set of metas. The [evar_reset_evd] function
+     below just replaces the metas of sigma by those coming from the clenv. *)
   let sigma = Tacmach.New.project gl in
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
-  (** Still, we need to update the universes *)
+  (* Still, we need to update the universes *)
   let clenv, c =
     if poly then
-      (** Refresh the instance of the hint *)
+      (* Refresh the instance of the hint *)
       let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
       let emap c = Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      (** Only metas are mentioning the old universes. *)
+      (* Only metas are mentioning the old universes. *)
       let clenv = {
         templval = Evd.map_fl emap clenv.templval;
         templtyp = Evd.map_fl emap clenv.templtyp;
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index fd2a163f80..ba7645446d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1096,8 +1096,8 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
 let initial_select_evars filter =
   fun evd ev evi ->
     filter ev (Lazy.from_val (snd evi.Evd.evar_source)) &&
-    (** Typeclass evars can contain evars whose conclusion is not
-        yet determined to be a class or not. *)
+    (* Typeclass evars can contain evars whose conclusion is not
+       yet determined to be a class or not. *)
     Typeclasses.is_class_evar evd evi
 
 let resolve_typeclass_evars debug depth unique env evd filter split fail =
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 46dff34f89..a6922213d0 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -39,20 +39,20 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
 module Search : sig
   val eauto_tac :
-    ?st:TransparentState.t ->
+    ?st:TransparentState.t
     (** The transparent_state used when working with local hypotheses  *)
-    ?unique:bool ->
+    -> ?unique:bool
     (** Should we force a unique solution *)
-    only_classes:bool ->
+    -> only_classes:bool
     (** Should non-class goals be shelved and resolved at the end *)
-    ?strategy:search_strategy ->
+    -> ?strategy:search_strategy
     (** Is a traversing-strategy specified? *)
-    depth:Int.t option ->
+    -> depth:Int.t option
     (** Bounded or unbounded search *)
-    dep:bool ->
+    -> dep:bool
     (** Should the tactic be made backtracking on the initial goals,
-       whatever their internal dependencies are. *)
-    Hints.hint_db list ->
+        whatever their internal dependencies are. *)
+    -> Hints.hint_db list
     (** The list of hint databases to use *)
-    unit Proofview.tactic
+    -> unit Proofview.tactic
 end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bdc95941b2..769e702da1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1742,7 +1742,7 @@ let subst_one_var dep_proof_ok x =
       (* Find a non-recursive definition for x *)
       let res =
         try
-          (** [is_eq_x] ensures nf_evar on its side *)
+          (* [is_eq_x] ensures nf_evar on its side *)
           let hyps = Proofview.Goal.hyps gl in
           let test hyp _ = is_eq_x gl x hyp in
           Context.Named.fold_outside test ~init:() hyps;
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 77479f9efa..c20feccace 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -210,9 +210,9 @@ let fresh_key =
     let lbl = Id.of_string ("_" ^ string_of_int cur) in
     let kn = Lib.make_kn lbl in
     let (mp, _) = KerName.repr kn in
-    (** We embed the full path of the kernel name in the label so that the
-        identifier should be unique. This ensures that including two modules
-        together won't confuse the corresponding labels. *)
+    (* We embed the full path of the kernel name in the label so that
+       the identifier should be unique. This ensures that including
+       two modules together won't confuse the corresponding labels. *)
     let lbl = Id.of_string_soft (Printf.sprintf "%s#%i"
       (ModPath.to_string mp) cur)
     in
@@ -558,7 +558,7 @@ struct
   let realize_tac secvars (id,tac) =
     if Id.Pred.subset tac.secvars secvars then Some tac
     else
-      (** Warn about no longer typable hint? *)
+      (* Warn about no longer typable hint? *)
       None
 
   let head_evar sigma c =
@@ -601,7 +601,7 @@ struct
     let se = find k db in
     merge_entry secvars db se.sentry_nopat se.sentry_pat
 	
-  (** Precondition: concl has no existentials *)
+  (* Precondition: concl has no existentials *)
   let map_auto sigma ~secvars (k,args) concl db =
     let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
@@ -644,7 +644,7 @@ struct
       | None ->
           let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in
 	  if not (List.exists is_present db.hintdb_nopat) then
-	    (** FIXME *)
+            (* FIXME *)
 	    { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
 	  else db
       | Some gr ->
@@ -738,7 +738,6 @@ module Hintdbmap = String.Map
 type hint_db = Hint_db.t
 
 (** Initially created hint databases, for typeclasses and rewrite *)
-
 let typeclasses_db = "typeclass_instances"
 let rewrite_db = "rewrite"
 
@@ -1586,7 +1585,7 @@ let log_hint h =
   let store = get_extra_data sigma in
   match Store.get store hint_trace with
   | None ->
-    (** All calls to hint logging should be well-scoped *)
+    (* All calls to hint logging should be well-scoped *)
     assert false
   | Some trace ->
     let trace = KNmap.add h.uid h trace in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6a39a10fc4..2ae37ab471 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -365,7 +365,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
   let substHypIfVariable tac id =
     Proofview.Goal.enter begin fun gl ->
     let sigma = project gl in
-    (** We only look at the type of hypothesis "id" *)
+    (* We only look at the type of hypothesis "id" *)
     let hyp = pf_nf_evar gl (pf_get_hyp_typ id gl) in
     let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in
     match (EConstr.kind sigma t1, EConstr.kind sigma t2) with
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 224cd68cf9..bfbce8f6eb 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -572,7 +572,7 @@ module New = struct
     with Failure _ -> CErrors.user_err Pp.(str "Not enough hypotheses in the goal.")
 
   let nthHypId m gl =
-    (** We only use [id] *)
+    (* We only use [id] *)
     nthDecl m gl |> NamedDecl.get_id
   let nthHyp m gl = 
     mkVar (nthHypId m gl)
@@ -688,12 +688,12 @@ module New = struct
     end) end
 
   let elimination_sort_of_goal gl =
-    (** Retyping will expand evars anyway. *)
+    (* Retyping will expand evars anyway. *)
     let c = Proofview.Goal.concl gl in
     pf_apply Retyping.get_sort_family_of gl c
 
   let elimination_sort_of_hyp id gl =
-    (** Retyping will expand evars anyway. *)
+    (* Retyping will expand evars anyway. *)
     let c = pf_get_hyp_typ id gl in
     pf_apply Retyping.get_sort_family_of gl c
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2947e44f7a..201b7801c3 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -191,6 +191,7 @@ module New : sig
   val tclTHENS3PARTS     : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic
   val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic
   val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic
+
   (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls]
       and [tac2] to the first resulting subgoal *)
   val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b3ea13cf4f..9e9d52b72c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -183,7 +183,7 @@ let convert_gen pb x y =
     | Some sigma -> Proofview.Unsafe.tclEVARS sigma
     | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
     | exception _ ->
-      (** FIXME: Sometimes an anomaly is raised from conversion *)
+      (* FIXME: Sometimes an anomaly is raised from conversion *)
       Tacticals.New.tclFAIL 0 (str "Not convertible")
 end
 
@@ -241,7 +241,7 @@ let clear_gen fail = function
 | ids ->
   Proofview.Goal.enter begin fun gl ->
     let ids = List.fold_right Id.Set.add ids Id.Set.empty in
-    (** clear_hyps_in_evi does not require nf terms *)
+    (* clear_hyps_in_evi does not require nf terms *)
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
@@ -307,7 +307,7 @@ let rename_hyp repl =
       let concl = Proofview.Goal.concl gl in
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
-      (** Check that we do not mess variables *)
+      (* Check that we do not mess variables *)
       let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in
       let vars = List.fold_left fold Id.Set.empty hyps in
       let () =
@@ -322,7 +322,7 @@ let rename_hyp repl =
           CErrors.user_err  (Id.print elt ++ str " is already used")
         with Not_found -> ()
       in
-      (** All is well *)
+      (* All is well *)
       let make_subst (src, dst) = (src, mkVar dst) in
       let subst = List.map make_subst repl in
       let subst c = Vars.replace_vars subst c in
@@ -1235,7 +1235,7 @@ let cut c =
     let concl = Proofview.Goal.concl gl in
     let is_sort =
       try
-        (** Backward compat: ensure that [c] is well-typed. *)
+        (* Backward compat: ensure that [c] is well-typed. *)
         let typ = Typing.unsafe_type_of env sigma c in
         let typ = whd_all env sigma typ in
         match EConstr.kind sigma typ with
@@ -1245,7 +1245,7 @@ let cut c =
     in
     if is_sort then
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
-      (** Backward compat: normalize [c]. *)
+      (* Backward compat: normalize [c]. *)
       let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
       Refine.refine ~typecheck:false begin fun h ->
         let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
@@ -1498,8 +1498,8 @@ let simplest_elim c = default_elim false None (c,NoBindings)
 *)
 
 let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
-  (** The evarmap of elimclause is assumed to be an extension of hypclause, so
-      we do not need to merge the universes coming from hypclause. *)
+  (* The evarmap of elimclause is assumed to be an extension of hypclause, so
+     we do not need to merge the universes coming from hypclause. *)
   try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause
   with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
     (* Set the hypothesis name in the message *)
@@ -1909,7 +1909,7 @@ let exact_no_check c =
 let exact_check c =
   Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
-  (** We do not need to normalize the goal because we just check convertibility *)
+  (* We do not need to normalize the goal because we just check convertibility *)
   let concl = Proofview.Goal.concl gl in
   let env = Proofview.Goal.env gl in
   let sigma, ct = Typing.type_of env sigma c in
@@ -2021,7 +2021,7 @@ let clear_body ids =
     let check =
       try
         let check (env, sigma, seen) decl =
-          (** Do no recheck hypotheses that do not depend *)
+          (* Do no recheck hypotheses that do not depend *)
           let sigma =
             if not seen then sigma
             else if List.exists (fun id -> occur_var_in_decl env sigma id decl) ids then
@@ -2848,7 +2848,7 @@ let generalize_dep ?(with_let=false) c =
   in
   let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
     (cl',project gl) in
-  (** Check that the generalization is indeed well-typed *)
+  (* Check that the generalization is indeed well-typed *)
   let (evd, _) = Typing.type_of env evd cl'' in
   let args = Context.Named.to_instance mkVar to_quantify_rev in
   tclTHENLIST
@@ -3021,7 +3021,7 @@ let specialize (c,lbind) ipat =
 let unfold_body x =
   let open Context.Named.Declaration in
   Proofview.Goal.enter begin fun gl ->
-  (** We normalize the given hypothesis immediately. *)
+  (* We normalize the given hypothesis immediately. *)
   let env = Proofview.Goal.env gl in
   let xval = match Environ.lookup_named x env with
   | LocalAssum _ -> user_err ~hdr:"unfold_body"
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 03d2a17eee..e273891500 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -281,7 +281,7 @@ struct
   open TDnet
 
   let pat_of_constr c : term_pattern =
-    (** To each evar we associate a unique identifier. *)
+    (* To each evar we associate a unique identifier. *)
     let metas = ref Evar.Map.empty in
     let rec pat_of_constr c = match Constr.kind c with
     | Rel _          -> Term DRel
@@ -378,7 +378,7 @@ struct
 	 let c_id = Opt.reduce (Ident.constr_of id) in
 	 let c_id = EConstr.of_constr c_id in
 	 let (ctx,wc) =
-	   try Termops.align_prod_letin Evd.empty whole_c c_id (** FIXME *)
+           try Termops.align_prod_letin Evd.empty whole_c c_id (* FIXME *)
 	   with Invalid_argument _ -> [],c_id in
 	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
 	 try
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 226a19678f..4e80caa4cc 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -233,7 +233,7 @@ struct
             let rem = NSet.fold push next rem in
             aux rem seen
           | Some false ->
-            (** The path we took encountered x -> y but not the one in seen *)
+            (* The path we took encountered x -> y but not the one in seen *)
             if through then aux (NMap.add n true rem) (NMap.add n true seen)
             else aux rem seen
           | Some true -> aux rem seen
@@ -357,7 +357,7 @@ let treat_coq_file chan =
           | None -> acc
           | Some file_str -> (canonize file_str, ".v") :: acc
         else acc
-      | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *)
+      | AddLoadPath _ | AddRecLoadPath _ -> acc (* TODO *)
       in
       loop acc
   in
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index db2031c64b..e3dd32fb63 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -132,7 +132,7 @@ let add_mllib_known, _, search_mllib_known = mkknown ()
 let add_mlpack_known, _, search_mlpack_known = mkknown ()
 
 let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t)
-(** The associated boolean is true if this is a root path. *)
+(* The associated boolean is true if this is a root path. *)
 let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
 
 let get_prefix p l =
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 6c4ea9afa1..0a32879764 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -176,7 +176,7 @@ let set_batch_mode opts =
 let add_compile opts verbose s =
   let opts = set_batch_mode opts in
   if not opts.glob_opt then Dumpglob.dump_to_dotglob ();
-  (** make the file name explicit; needed not to break up Coq loadpath stuff. *)
+  (* make the file name explicit; needed not to break up Coq loadpath stuff. *)
   let s =
     let open Filename in
     if is_implicit s
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index edef741ca6..56622abc92 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -95,9 +95,9 @@ let init_color opts =
     if has_color then begin
       let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
       match colors with
-      | None -> Topfmt.default_styles (); true        (** Default colors *)
-      | Some "" -> false                              (** No color output *)
-      | Some s -> Topfmt.parse_color_config s; true   (** Overwrite all colors *)
+      | None -> Topfmt.default_styles (); true        (* Default colors *)
+      | Some "" -> false                              (* No color output *)
+      | Some s -> Topfmt.parse_color_config s; true   (* Overwrite all colors *)
     end
     else
       false
@@ -144,7 +144,7 @@ let init_gc () =
      * In this case, we put in place our preferred configuration.
      *)
     Gc.set { (Gc.get ()) with
-             Gc.minor_heap_size = 33554432; (** 4M *)
+             Gc.minor_heap_size = 33554432; (* 4M *)
              Gc.space_overhead = 120}
 
 (** Main init routine *)
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 3ca2a4ad6b..b5cc74b594 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -294,7 +294,7 @@ let traverse current t =
 let type_of_constant cb = cb.Declarations.const_type
 
 let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
-  (** Only keep the transitive dependencies *)
+  (* Only keep the transitive dependencies *)
   let (_, graph, ax2ty) = traverse (label_of gr) t in
   let fold obj _ accu = match obj with
   | VarRef id ->
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 6a32960a9d..66e10f94cd 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -119,6 +119,7 @@ val vernac_monomorphic_flag : vernac_flag
 (** For the stm, do not use! *)
 
 val polymorphic_nowarn : bool attribute
+
 (** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *)
 val universe_polymorphism_option_name : string list
 val is_universe_polymorphism : unit -> bool
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index fa1b8eeb3e..d9787bc73c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -335,8 +335,8 @@ let build_beq_scheme mode kn =
         | Finite ->
           mkFix (((Array.make nb_ind 0),i),(names,types,cores))
         | BiFinite ->
-          (** If the inductive type is not recursive, the fixpoint is not
-              used, so let's replace it with garbage *)
+          (* If the inductive type is not recursive, the fixpoint is
+             not used, so let's replace it with garbage *)
           let subst = List.init nb_ind (fun _ -> mkProp) in
           Vars.substl subst cores.(i)
         in
diff --git a/vernac/class.ml b/vernac/class.ml
index ab43d5c8ff..8374a5c84f 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -66,7 +66,7 @@ let explain_coercion_error g = function
 let check_reference_arity ref =
   let env = Global.env () in
   let c, _ = Typeops.type_of_global_in_context env ref in
-  if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (** FIXME *) then
+  if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (* FIXME *) then
     raise (CoercionError (NotAClass ref))
 
 let check_arity = function
@@ -260,7 +260,7 @@ let add_new_coercion_core coef stre poly source target isid =
       raise (CoercionError (NoSource source))
   in
   check_source (Some cls);
-  if not (uniform_cond Evd.empty (** FIXME - for when possibly called with unresolved evars in the future *)
+  if not (uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *)
                        ctx lvs) then
     warn_uniform_inheritance coef;
   let clt =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d0cf1c6bee..370df615fc 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -373,7 +373,7 @@ let context poly l =
     | [] -> assert false
     | [_] -> Evd.const_univ_entry ~poly sigma
     | _::_::_ ->
-      (** TODO: explain this little belly dance *)
+      (* TODO: explain this little belly dance *)
       if Lib.sections_are_opened ()
       then
         begin
diff --git a/vernac/classes.mli b/vernac/classes.mli
index bb70334342..eb6c0c92e1 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -27,22 +27,22 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 
 val declare_instance_constant :
   typeclass ->
-  Hints.hint_info_expr -> (** priority *)
-  bool -> (** globality *)
-  Impargs.manual_explicitation list -> (** implicits *)
+  Hints.hint_info_expr (** priority *) ->
+  bool (** globality *) ->
+  Impargs.manual_explicitation list (** implicits *) ->
   ?hook:(GlobRef.t -> unit) ->
-  Id.t -> (** name *)
+  Id.t (** name *) ->
   UState.universe_decl ->
-  bool -> (* polymorphic *)
-  Evd.evar_map -> (* Universes *)
-  Constr.t -> (** body *)
-  Constr.types -> (** type *)
+  bool (** polymorphic *) ->
+  Evd.evar_map (** Universes *) ->
+  Constr.t (** body *) ->
+  Constr.types (** type *) ->
   unit
 
 val new_instance :
-  ?abstract:bool -> (** Not abstract by default. *)
-  ?global:bool -> (** Not global by default. *)
-  ?refine:bool -> (** Allow refinement *)
+  ?abstract:bool (** Not abstract by default. *) ->
+  ?global:bool (** Not global by default. *) ->
+  ?refine:bool (** Allow refinement *) ->
   program_mode:bool ->
   Decl_kinds.polymorphic ->
   local_binder_expr list ->
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index f4569ed3e2..338dfa5ef5 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -78,6 +78,7 @@ val interp_fixpoint :
   (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
+
 (** [Not used so far] *)
 val declare_fixpoint :
   locality -> polymorphic ->
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8b9cf7d269..4af6415a4d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -265,7 +265,7 @@ let inductive_levels env evd poly arities inds =
           else minlev
         in
         let minlev =
-          (** Indices contribute. *)
+          (* Indices contribute. *)
           if indices_matter env && List.length ctx > 0 then (
             let ilev = sign_level env evd ctx in
               Univ.sup ilev minlev)
@@ -282,15 +282,15 @@ let inductive_levels env evd poly arities inds =
   let evd, arities =
     CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
       if is_impredicative env du then
-        (** Any product is allowed here. *)
+        (* Any product is allowed here. *)
         evd, arity :: arities
-      else (** If in a predicative sort, or asked to infer the type,
-               we take the max of:
-               - indices (if in indices-matter mode)
-               - constructors
-               - Type(1) if there is more than 1 constructor
+      else (* If in a predicative sort, or asked to infer the type,
+              we take the max of:
+              - indices (if in indices-matter mode)
+              - constructors
+              - Type(1) if there is more than 1 constructor
            *)
-        (** Constructors contribute. *)
+        (* Constructors contribute. *)
         let evd =
           if Sorts.is_set du then
             if not (Evd.check_leq evd cu Univ.type0_univ) then
@@ -301,7 +301,7 @@ let inductive_levels env evd poly arities inds =
         in
         let evd =
           if len >= 2 && Univ.is_type0m_univ cu then
-           (** "Polymorphic" type constraint and more than one constructor,
+           (* "Polymorphic" type constraint and more than one constructor,
                should not land in Prop. Add constraint only if it would
                land in Prop directly (no informative arguments as well). *)
             Evd.set_leq_sort env evd Set du
@@ -510,7 +510,7 @@ let is_recursive mie =
   let rec is_recursive_constructor lift typ =
     match Constr.kind typ with
     | Prod (_,arg,rest) ->
-        not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) ||
+        not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) ||
         is_recursive_constructor (lift+1) rest
     | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest
     | _ -> false
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index f23085a538..9df8f7c341 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -39,8 +39,8 @@ val do_mutual_inductive :
    associated schemes *)
 
 type one_inductive_impls =
-  Impargs.manual_implicits (** for inds *)*
-  Impargs.manual_implicits list (** for constrs *)
+  Impargs.manual_implicits (* for inds *) *
+  Impargs.manual_implicits list (* for constrs *)
 
 val declare_mutual_inductive_with_eliminations :
   mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index e62ae99159..edce8e255c 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -211,7 +211,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         let univs = Evd.check_univ_decl ~poly sigma decl in
         (*FIXME poly? *)
         let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
-        (** FIXME: include locality *)
+        (* FIXME: include locality *)
         let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
         let gr = ConstRef c in
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 898de7b166..41057f8ab2 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -27,7 +27,7 @@ let warn_local_declaration =
 
 let get_locality id ~kind = function
 | Discharge ->
-  (** If a Let is defined outside a section, then we consider it as a local definition *)
+  (* If a Let is defined outside a section, then we consider it as a local definition *)
    warn_local_declaration (id,kind);
   true
 | Local -> true
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 6c7117b513..68d6db75ee 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -125,12 +125,12 @@ let display_eq ~flags env sigma t1 t2 =
     printed alike. *)
 let rec pr_explicit_aux env sigma t1 t2 = function
 | [] ->
-  (** no specified flags: default. *)
+  (* no specified flags: default. *)
   (quote (Printer.pr_leconstr_env env sigma t1), quote (Printer.pr_leconstr_env env sigma t2))
 | flags :: rem ->
   let equal = display_eq ~flags env sigma t1 t2 in
   if equal then
-    (** The two terms are the same from the user point of view *)
+    (* The two terms are the same from the user point of view *)
     pr_explicit_aux env sigma t1 t2 rem
   else
     let open Constrextern in
@@ -142,12 +142,12 @@ let rec pr_explicit_aux env sigma t1 t2 = function
 
 let explicit_flags =
   let open Constrextern in
-  [ []; (** First, try with the current flags *)
-    [print_implicits]; (** Then with implicit *)
-    [print_universes]; (** Then with universes *)
-    [print_universes; print_implicits]; (** With universes AND implicits *)
-    [print_implicits; print_coercions; print_no_symbol]; (** Then more! *)
-    [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ]
+  [ []; (* First, try with the current flags *)
+    [print_implicits]; (* Then with implicit *)
+    [print_universes]; (* Then with universes *)
+    [print_universes; print_implicits]; (* With universes AND implicits *)
+    [print_implicits; print_coercions; print_no_symbol]; (* Then more! *)
+    [print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ]
 
 let pr_explicit env sigma t1 t2 =
   pr_explicit_aux env sigma t1 t2 explicit_flags
@@ -328,7 +328,7 @@ let explain_actual_type env sigma j t reason =
   let env = make_all_name_different env sigma in
   let j = j_nf_betaiotaevar env sigma j in
   let t = Reductionops.nf_betaiota env sigma t in
-  (** Actually print *)
+  (* Actually print *)
   let pe = pr_ne_context_of (str "In environment") env sigma in
   let pc = pr_leconstr_env env sigma (Environ.j_val j) in
   let (pt, pct) = pr_explicit env sigma t (Environ.j_type j) in
@@ -774,7 +774,7 @@ let explain_unsatisfiable_constraints env sigma constr comp =
   let (_, constraints) = Evd.extract_all_conv_pbs sigma in
   let tcs = Evd.get_typeclass_evars sigma in
   let undef = Evd.undefined_map sigma in
-  (** Only keep evars that are subject to resolution and members of the given
+  (* Only keep evars that are subject to resolution and members of the given
      component. *)
   let is_kept evk _ = match comp with
   | None -> Evar.Set.mem evk tcs
@@ -1112,7 +1112,7 @@ let error_ill_formed_inductive env c v =
 
 let error_ill_formed_constructor env id c v nparams nargs =
   let pv = pr_lconstr_env env (Evd.from_env env) v in
-  let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in
+  let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (* FIXME *) 0 in
   str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++
   str "is not valid;" ++ brk(1,1) ++
   strbrk (if atomic then "it must be " else "its conclusion must be ") ++
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 9bd095aa52..d29f66f81f 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -307,7 +307,7 @@ let warn_cannot_build_congruence =
           strbrk "Cannot build congruence scheme because eq is not found")
 
 let declare_congr_scheme ind =
-  if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (** FIXME *) then begin
+  if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin
     if
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with e when CErrors.noncritical e -> false
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 82434afbbd..dccd776fa8 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1467,7 +1467,7 @@ let add_notation_in_scope local df env c mods scope =
     notobj_local = local;
     notobj_scope = scope;
     notobj_interp = (List.map_filter map i_vars, ac);
-    (** Order is important here! *)
+    (* Order is important here! *)
     notobj_onlyparse = onlyparse;
     notobj_coercion = coe;
     notobj_onlyprint = sd.only_printing;
@@ -1486,7 +1486,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
   let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
     let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
     let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
-    (** If the only printing flag has been explicitly requested, put it back *)
+    (* If the only printing flag has been explicitly requested, put it back *)
     let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
     let _,_,_,typs = sy.synext_level in
     Some sy.synext_level, typs, onlyprint
@@ -1507,7 +1507,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
     notobj_local = local;
     notobj_scope = scope;
     notobj_interp = (List.map_filter map i_vars, ac);
-    (** Order is important here! *)
+    (* Order is important here! *)
     notobj_onlyparse = onlyparse;
     notobj_coercion = coe;
     notobj_onlyprint = onlyprint;
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index f18227039f..6642d04c98 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -381,7 +381,7 @@ let subst_deps expand obls deps t =
     (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
 
 let rec prod_app t n =
-  match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with
+  match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (* FIXME *) with
     | Prod (_,_,b) -> subst1 n b
     | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
     | _ ->
@@ -503,7 +503,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (** FIXME *) in
+      let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in
       let ctx = fst (decompose_prod_n_assum m fixtype) in
 	List.map_i (fun i _ -> i) 0 ctx
 
@@ -649,7 +649,7 @@ let declare_obligation prg obl body ty uctx =
           const_entry_inline_code = false;
           const_entry_feedback = None;
       } in
-      (** ppedrot: seems legit to have obligations as local *)
+      (* ppedrot: seems legit to have obligations as local *)
       let constant = Declare.declare_constant obl.obl_name ~local:true
 	(DefinitionEntry ce,IsProof Property)
       in
@@ -857,9 +857,9 @@ let obligation_terminator ?univ_hook name num guard auto pf =
     let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
     Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
-    (** Declare the obligation ourselves and drop the hook *)
+    (* Declare the obligation ourselves and drop the hook *)
     let prg = get_info (ProgMap.find name !from_prg) in
-    (** Ensure universes are substituted properly in body and type *)
+    (* Ensure universes are substituted properly in body and type *)
     let body = EConstr.to_constr sigma (EConstr.of_constr body) in
     let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
     let ctx = Evd.evar_universe_context sigma in
@@ -885,14 +885,14 @@ let obligation_terminator ?univ_hook name num guard auto pf =
     let () = obls.(num) <- obl in
     let prg_ctx =
       if pi2 (prg.prg_kind) then (* Polymorphic *)
-        (** We merge the new universes and constraints of the
-            polymorphic obligation with the existing ones *)
+        (* We merge the new universes and constraints of the
+           polymorphic obligation with the existing ones *)
         UState.union prg.prg_ctx ctx
       else
-        (** The first obligation, if defined,
-            declares the univs of the constant,
-            each subsequent obligation declares its own additional
-            universes and constraints if any *)
+        (* The first obligation, if defined,
+           declares the univs of the constant,
+           each subsequent obligation declares its own additional
+           universes and constraints if any *)
         if defined then UState.make (Global.universes ())
         else ctx
     in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e7c1e29beb..8535585749 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -363,7 +363,7 @@ open Pputils
       match factorize l with
         | (xl,((c', t') as r))::l'
             when (c : bool) == c' && Pervasives.(=) t t' ->
-          (** FIXME: we need equality on constr_expr *)
+          (* FIXME: we need equality on constr_expr *)
           (idl@xl,r)::l'
         | l' -> (idl,(c,t))::l'
 
diff --git a/vernac/record.ml b/vernac/record.ml
index f6dbcb5291..ffd4f654c6 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -321,7 +321,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
                     ~proj_arg:i
                     (Label.of_id fid)
                 in
-                (** Already defined by declare_mind silently *)
+                (* Already defined by declare_mind silently *)
                 let kn = Projection.Repr.constant p in
                 Declare.definition_message fid;
                 kn, mkProj (Projection.make p false,mkRel 1)
diff --git a/vernac/search.ml b/vernac/search.ml
index 1fac28358a..6610789626 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -172,8 +172,8 @@ let prioritize_search seq fn =
 
 (** Filters *)
 
-(** This function tries to see whether the conclusion matches a pattern. *)
-(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
+(** This function tries to see whether the conclusion matches a pattern.
+    FIXME: this is quite dummy, we may find a more efficient algorithm. *)
 let rec pattern_filter pat ref env sigma typ =
   let typ = Termops.strip_outer_cast sigma typ in
   if Constr_matching.is_matching env sigma pat typ then true
diff --git a/vernac/search.mli b/vernac/search.mli
index 0dc82c1c3f..ecbb02bc68 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -49,16 +49,16 @@ val search_about   : int option -> (bool * glob_search_about_item) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
-  (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
   | Name_Pattern of Str.regexp
-  (** Whether the object type satisfies a pattern *)
+  (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
   | Type_Pattern of Pattern.constr_pattern
-  (** Whether some subtype of object type satisfies a pattern *)
+  (** Whether the object type satisfies a pattern *)
   | SubType_Pattern of Pattern.constr_pattern
-  (** Whether the object pertains to a module *)
+  (** Whether some subtype of object type satisfies a pattern *)
   | In_Module of Names.DirPath.t
-  (** Bypass the Search blacklist *)
+  (** Whether the object pertains to a module *)
   | Include_Blacklist
+  (** Bypass the Search blacklist *)
 
 type 'a coq_object = {
   coq_object_prefix : string list;
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 4bf76dae51..4065bb9c1f 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -222,20 +222,21 @@ let diff_tag_stack = ref []  (* global, just like std_ft *)
 (** Not thread-safe. We should put a lock somewhere if we print from
     different threads. Do we? *)
 let make_style_stack () =
-  (** Default tag is to reset everything *)
+  (* Default tag is to reset everything *)
   let style_stack = ref [] in
   let peek () = match !style_stack with
-  | []      -> default_style  (** Anomalous case, but for robustness *)
+  | []      -> default_style  (* Anomalous case, but for robustness *)
   | st :: _ -> st
   in
   let open_tag tag =
     let (tpfx, ttag) = split_tag tag in
     if tpfx = end_pfx then "" else
       let style = get_style ttag in
-    (** Merge the current settings and the style being pushed.  This allows
-    restoring the previous settings correctly in a pop when both set the same
-    attribute.  Example: current settings have red FG, the pushed style has
-    green FG.  When popping the style, we should set red FG, not default FG. *)
+      (* Merge the current settings and the style being pushed.  This
+         allows restoring the previous settings correctly in a pop
+         when both set the same attribute.  Example: current settings
+         have red FG, the pushed style has green FG.  When popping the
+         style, we should set red FG, not default FG. *)
     let style = Terminal.merge (peek ()) style in
     let diff = Terminal.diff (peek ()) style in
     style_stack := style :: !style_stack;
@@ -247,7 +248,7 @@ let make_style_stack () =
       if tpfx = start_pfx then "" else begin
         if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []);
         match !style_stack with
-        | []       -> (** Something went wrong, we fallback *)
+        | []       -> (* Something went wrong, we fallback *)
                       Terminal.eval default_style
         | cur :: rem -> style_stack := rem;
                       if cur = (peek ()) then "" else
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f5d68a2199..3fa3681661 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -681,14 +681,14 @@ let vernac_inductive ~atts cum lo finite indl =
   | _ -> None
   in
   if Option.has_some is_defclass then
-    (** Definitional class case *)
+    (* Definitional class case *)
     let (id, bl, c, l) = Option.get is_defclass in
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
     let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
     vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
-    (** Mutual record case *)
+    (* Mutual record case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
     | Variant ->
       user_err (str "The Variant keyword does not support syntax { ... }.")
@@ -704,14 +704,14 @@ let vernac_inductive ~atts cum lo finite indl =
     let unpack ((id, bl, c, _, decl), _) = match decl with
     | RecordDecl (oc, fs) ->
       (id, bl, c, oc, fs)
-    | Constructors _ -> assert false (** ruled out above *)
+    | Constructors _ -> assert false (* ruled out above *)
     in
     let ((_, _, _, kind, _), _) = List.hd indl in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
     vernac_record ~template udecl cum kind atts.polymorphic finite recordl
   else if List.for_all is_constructor indl then
-    (** Mutual inductive case *)
+    (* Mutual inductive case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
     | (Record | Structure) ->
       user_err (str "The Record keyword is for types defined using the syntax { ... }.")
@@ -1992,7 +1992,7 @@ let vernac_search ~atts s gopt r =
 let vernac_locate = function
   | LocateAny {v=AN qid}  -> print_located_qualid qid
   | LocateTerm {v=AN qid} -> print_located_term qid
-  | LocateAny {v=ByNotation (ntn, sc)} (** TODO : handle Ltac notations *)
+  | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
   | LocateTerm {v=ByNotation (ntn, sc)} ->
     let _, env = Pfedit.get_current_context () in
     Notation.locate_notation
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 1e6c40c829..417c9ebfbd 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -247,11 +247,11 @@ type vernac_argument_status = {
 }
 
 type extend_name =
-  (** Name of the vernac entry where the tactic is defined, typically found
-      after the VERNAC EXTEND statement in the source. *)
+  (* Name of the vernac entry where the tactic is defined, typically found
+     after the VERNAC EXTEND statement in the source. *)
   string *
-  (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch
-      is given an offset, starting from zero. *)
+  (* Index of the extension in the VERNAC EXTEND statement. Each parsing branch
+     is given an offset, starting from zero. *)
   int
 
 type nonrec vernac_expr =
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 2541f73582..05687afd8b 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -42,8 +42,11 @@ and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+
 and solving_tac = bool (** a terminator *)
+
 and anon_abstracting_tac = bool (** abstracting anonymously its result *)
+
 and proof_block_name = string (** open type of delimiters *)
 
 type vernac_when =
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 8b07be8b16..0d43eb1ee8 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -58,8 +58,11 @@ and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+
 and solving_tac = bool (** a terminator *)
+
 and anon_abstracting_tac = bool (** abstracting anonymously its result *)
+
 and proof_block_name = string (** open type of delimiters *)
 
 type vernac_when =
@@ -86,7 +89,7 @@ type (_, _) ty_sig =
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
     ('a -> 'r, 'a -> 's) ty_sig
 
-type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+type ty_ml = TyML : bool (* deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml
 
 (** Wrapper to dynamically extend vernacular commands. *)
 val vernac_extend :