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

11 files changed, 50 insertions, 50 deletions

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