[doc] Enable Warning 50 [incorrect doc comment] and fix comments.

This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.

p.s: Reading some comments was a lot of fun :)

24 files changed, 92 insertions, 83 deletions

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 :