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

1 files changed, 4 insertions, 4 deletions

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