Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.

5 files changed, 14 insertions, 13 deletions

diff --git a/checker/analyze.ml b/checker/analyze.ml
index 7047d8a149..63324bff20 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -396,7 +396,7 @@ let parse_string s = PString.parse (s, ref 0)
 let instantiate (p, mem) =
   let len = LargeArray.length mem in
   let ans = LargeArray.make len (Obj.repr 0) in
-  (** First pass: initialize the subobjects *)
+  (* First pass: initialize the subobjects *)
   for i = 0 to len - 1 do
     let obj = match LargeArray.get mem i with
     | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
@@ -408,9 +408,9 @@ let instantiate (p, mem) =
   | Int n -> Obj.repr n
   | Ptr p -> LargeArray.get ans p
   | Atm tag -> Obj.new_block tag 0
-  | Fun _ -> assert false (** We shouldn't serialize closures *)
+  | Fun _ -> assert false (* We shouldn't serialize closures *)
   in
-  (** Second pass: set the pointers *)
+  (* Second pass: set the pointers *)
   for i = 0 to len - 1 do
     match LargeArray.get mem i with
     | Struct (_, blk) ->
diff --git a/checker/analyze.mli b/checker/analyze.mli
index 9c837643fa..d7770539df 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -30,6 +30,7 @@ sig
   type t
   val input_byte : t -> int
   (** Input a single byte *)
+
   val input_binary_int : t -> int
   (** Input a big-endian 31-bits signed integer *)
 end
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 4e026d6f60..ef10bf827d 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -95,11 +95,11 @@ let typecheck_arity env params inds =
 (* Check that the subtyping information inferred for inductive types in the block is correct. *)
 (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
 let check_subtyping cumi paramsctxt env arities =
-    let numparams = Context.Rel.nhyps paramsctxt in
-  (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
-      We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
-      and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
-      with the cumulativity constraints [ cumul_cst ]. *)
+  let numparams = Context.Rel.nhyps paramsctxt in
+  (* In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
+     We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
+     and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
+     with the cumulativity constraints [ cumul_cst ]. *)
   let uctx = ACumulativityInfo.univ_context cumi in
   let len = AUContext.size uctx in
   let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in
@@ -238,7 +238,7 @@ let check_inductive env kn mib =
       let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in
       Environ.push_context uctx env
   in
-  (** Locally set the oracle for further typechecking *)
+  (* Locally set the oracle for further typechecking *)
   let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b83fe831bb..086dd17e39 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -10,10 +10,10 @@ open Environ
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  (** Locally set the oracle for further typechecking *)
+  (* Locally set the oracle for further typechecking *)
   let oracle = env.env_typing_flags.conv_oracle in
   let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
-  (** [env'] contains De Bruijn universe variables *)
+  (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
     | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
@@ -40,7 +40,7 @@ let check_constant_declaration env kn cb =
     if poly then add_constant kn cb env
     else add_constant kn cb env'
   in
-  (** Reset the value of the oracle *)
+  (* Reset the value of the oracle *)
   Environ.set_oracle env oracle
 
 (** {6 Checking modules } *)
diff --git a/checker/votour.ml b/checker/votour.ml
index 1ea0de456e..3c088b59b5 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -366,7 +366,7 @@ let visit_vo f =
   |] in
   let repr =
     if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S)
-    (** On 32-bit machines, representation may exceed the max size of arrays *)
+    (* On 32-bit machines, representation may exceed the max size of arrays *)
   in
   let module Repr = (val repr : S) in
   let module Visit = Visit(Repr) in