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

13 files changed, 38 insertions, 37 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 77d612cfd9..757d186c8b 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -80,8 +80,8 @@ type cases_pattern_expr_r =
 and cases_pattern_expr = cases_pattern_expr_r CAst.t
 
 and cases_pattern_notation_substitution =
-    cases_pattern_expr list *     (** for constr subterms *)
-    cases_pattern_expr list list  (** for recursive notations *)
+    cases_pattern_expr list *     (* for constr subterms *)
+    cases_pattern_expr list list  (* for recursive notations *)
 
 and constr_expr_r =
   | CRef     of qualid * instance_expr option
@@ -142,10 +142,10 @@ and local_binder_expr =
   | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
 
 and constr_notation_substitution =
-    constr_expr list *      (** for constr subterms *)
-    constr_expr list list * (** for recursive notations *)
-    cases_pattern_expr list *   (** for binders *)
-    local_binder_expr list list (** for binder lists (recursive notations) *)
+    constr_expr list *      (* for constr subterms *)
+    constr_expr list list * (* for recursive notations *)
+    cases_pattern_expr list *   (* for binders *)
+    local_binder_expr list list (* for binder lists (recursive notations) *)
 
 type constr_pattern_expr = constr_expr
 
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3a4969a3ee..3a5af1dd5f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 =
       in
       List.equal field_eq l1 l2
     | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
-      (** Don't care about the case_style *)
+      (* Don't care about the case_style *)
       Option.equal constr_expr_eq r1 r2 &&
       List.equal case_expr_eq a1 a2 &&
       List.equal branch_expr_eq brl1 brl2
@@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with
   | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
     eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
   | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
-    (** Don't care about the [binder_kind] *)
+    (* Don't care about the [binder_kind] *)
     List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
   | _ -> false
 
@@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with
   | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll))
 
 (** Folds and maps *)
-
 let is_constructor id =
   try Globnames.isConstructRef
         (Smartlocate.global_of_extended_global
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fba03b9de9..0d0b6158d9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -960,7 +960,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
 
   | GSort s -> CSort (extern_glob_sort s)
 
-  | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *)
+  | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *)
 
   | GCast (c, c') ->
       CCast (sub_extern true scopes vars c,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6313f2d7ba..40922b5c35 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1507,7 +1507,7 @@ let drop_notations_pattern looked_for genv =
   let test_kind top =
     if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
   in
-  (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+  (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
   let rec rcp_of_glob scopes x = DAst.(map (function
     | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
     | GHole (_,_,_) -> RCPatAtom (None)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 035e4bc644..61acd09d65 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -45,13 +45,15 @@ type var_internalization_type =
 
 type var_internalization_data =
     var_internalization_type *
-      (** type of the "free" variable, for coqdoc, e.g. while typing the
-	  constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+      (* type of the "free" variable, for coqdoc, e.g. while typing the
+         constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+
     Id.t list *
-      (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
-          in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
-    Impargs.implicit_status list * (** signature of impargs of the variable *)
-    Notation_term.scope_name option list (** subscopes of the args of the variable *)
+      (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+         in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+
+    Impargs.implicit_status list * (* signature of impargs of the variable *)
+    Notation_term.scope_name option list (* subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
 type internalization_env = var_internalization_data Id.Map.t
diff --git a/interp/declare.ml b/interp/declare.ml
index a809a856b9..a0ebc3775e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -56,7 +56,7 @@ let load_constant i ((sp,kn), obj) =
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn), obj) =
-  (** Never open a local definition *)
+  (* Never open a local definition *)
   if obj.cst_locl then ()
   else
     let con = Global.constant_of_delta_kn kn in
@@ -166,9 +166,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
         export_seff ||
         not de.const_entry_opaque ||
         is_poly de ->
-      (** This globally defines the side-effects in the environment. We mark
-          exported constants as being side-effect not to redeclare them at
-          caching time. *)
+      (* This globally defines the side-effects in the environment. We mark
+         exported constants as being side-effect not to redeclare them at
+         caching time. *)
       let de, export = Global.export_private_constants ~in_section de in
       export, ConstantEntry (PureEntry, DefinitionEntry de)
     | _ -> [], ConstantEntry (EffectEntry, cd)
@@ -191,7 +191,6 @@ let declare_definition ?(internal=UserIndividualRequest)
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of section variables and local definitions *)
-
 type section_variable_entry =
   | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
@@ -214,16 +213,16 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       let (de, eff) = Global.export_private_constants ~in_section:true de in
       let () = List.iter register_side_effect eff in
-      (** The body should already have been forced upstream because it is a
-          section-local definition, but it's not enforced by typing *)
+      (* The body should already have been forced upstream because it is a
+         section-local definition, but it's not enforced by typing *)
       let (body, uctx), () = Future.force de.const_entry_body in
       let poly, univs = match de.const_entry_universes with
       | Monomorphic_const_entry uctx -> false, uctx
       | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
       let univs = Univ.ContextSet.union uctx univs in
-      (** We must declare the universe constraints before type-checking the
-          term. *)
+      (* We must declare the universe constraints before type-checking the
+         term. *)
       let () = Global.push_context_set (not poly) univs in
       let se = {
         secdef_body = body;
@@ -262,7 +261,6 @@ let declare_variable id obj =
   oname
 
 (** Declaration of inductive blocks *)
-
 let declare_inductive_argument_scopes kn mie =
   List.iteri (fun i {mind_entry_consnames=lc} ->
     Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i));
@@ -360,7 +358,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
   let id = Label.to_id label in
   let univs = match univs with
     | Monomorphic_ind_entry _ ->
-      (** Global constraints already defined through the inductive *)
+      (* Global constraints already defined through the inductive *)
       Monomorphic_const_entry Univ.ContextSet.empty
     | Polymorphic_ind_entry (nas, ctx) ->
       Polymorphic_const_entry (nas, ctx)
@@ -511,7 +509,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
       load_function = load_univ_names;
       open_function = open_univ_names;
       discharge_function = discharge_univ_names;
-      subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
+      subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
 
 let declare_univ_binders gr pl =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 931d05a975..554da7603f 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -18,6 +18,7 @@ val dump : unit -> bool
 
 val noglob : unit -> unit
 val dump_into_file : string -> unit (** special handling of "stdout" *)
+
 val dump_to_dotglob : unit -> unit
 val feedback_glob : unit -> unit
 
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d024a9e808..8a89bcdf26 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -448,7 +448,7 @@ let compute_mib_implicits flags kn =
     Array.to_list
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
         (fun i mip ->
-	  (** No need to care about constraints here *)
+          (* No need to care about constraints here *)
           let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
 	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
         mib.mind_packets) in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ea5aa90f68..4afc2af5e9 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -65,6 +65,7 @@ type implicit_explanation =
      operational only if [conclusion_matters] is true. *)
 
 type maximal_insertion = bool (** true = maximal contextual insertion *)
+
 type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
 
 type implicit_status = (Id.t * implicit_explanation * 
diff --git a/interp/notation.ml b/interp/notation.ml
index 0af75b5bfa..e17cc65042 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -308,7 +308,7 @@ let declare_delimiters scope key =
     | None -> scope_map := String.Map.add scope newsc !scope_map
     | Some oldkey when String.equal oldkey key -> ()
     | Some oldkey ->
-        (** FIXME: implement multikey scopes? *)
+        (* FIXME: implement multikey scopes? *)
 	Flags.if_verbose Feedback.msg_info
 	  (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
 	scope_map := String.Map.add scope newsc !scope_map
diff --git a/interp/notation.mli b/interp/notation.mli
index 3480d1c8f2..ab0501a1e1 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool
 (** Open scope *)
 
 val open_close_scope :
-  (** locality *) bool * (* open *) bool * scope_name -> unit
+  (* locality *) bool * (* open *) bool * scope_name -> unit
 
 (** Extend a list of scopes *)
 val empty_scope_stack : scopes
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7a525f84a5..55a87fcd4d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -37,7 +37,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
    | _             -> false)
 | NApp (t1, a1), NApp (t2, a2) ->
   (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
-| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
+| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *)
 | NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
   Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
   (eq_notation_constr vars) u1 u2 && b1 == b2
@@ -51,7 +51,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
 | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
   Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
   Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
+| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
   let eqpat (p1, t1) (p2, t2) =
     List.equal cases_pattern_eq p1 p2 &&
     (eq_notation_constr vars) t1 t2
@@ -75,7 +75,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
   Option.equal (eq_notation_constr vars) o1 o2 &&
   (eq_notation_constr vars) u1 u2 &&
   (eq_notation_constr vars) r1 r2
-| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
+| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
   let eq (na1, o1, t1) (na2, o2, t2) =
     Name.equal na1 na2 &&
     Option.equal (eq_notation_constr vars) o1 o2 &&
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 5fb0ca1b43..0ef1f267f6 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -20,13 +20,13 @@ open Glob_term
     as well as non global expressions such as existential variables. *)
 
 type notation_constr =
-  (** Part common to [glob_constr] and [cases_pattern] *)
+  (* Part common to [glob_constr] and [cases_pattern] *)
   | NRef of GlobRef.t
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
-  (** Part only in [glob_constr] *)
+  (* Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
   | NProd of Name.t * notation_constr * notation_constr
   | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool