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

15 files changed, 66 insertions, 51 deletions

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 6aecc368e6..05bef91f1e 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 1019f8f0c2..39a9a8a3a5 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -37,8 +37,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 =