[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 :)

20 files changed, 83 insertions, 74 deletions

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 33ced6d6e0..0b545dc191 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -688,7 +688,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 f5e48bcd39..74ef1ddbca 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