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

10 files changed, 60 insertions, 54 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 603dd60cf2..ec2adf065a 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -306,8 +306,8 @@ let add_rewrite_hint ~poly bases ort t lcsr =
     let ctx =
       let ctx = UState.context_set ctx in
         if poly then ctx
-	else (** This is a global universe context that shouldn't be
-	       refreshed at every use of the hint, declare it globally. *)
+	else (* This is a global universe context that shouldn't be
+	        refreshed at every use of the hint, declare it globally. *)
 	  (Declare.declare_universe_context false ctx;
            Univ.ContextSet.empty)
     in
@@ -738,7 +738,8 @@ let  mkCaseEq a  : unit Proofview.tactic =
           Proofview.Goal.enter begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
-            (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
+            (* FIXME: this looks really wrong. Does anybody really use
+               this tactic? *)
             let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
 	    change_concl c
           end;
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index ef18dd6cdc..1ea6ff84d4 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -24,7 +24,7 @@ let (set_default_tactic, get_default_tactic, print_default_tactic) =
   Tactic_option.declare_tactic_option "Program tactic"
 
 let () =
-  (** Delay to recover the tactic imperatively *)
+  (* Delay to recover the tactic imperatively *)
   let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
     snd (get_default_tactic ())
   end in
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 55e58187b0..2267d43d93 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -235,8 +235,8 @@ let string_of_genarg_arg (ArgumentType arg) =
   let pr_tacarg_using_rule pr_gen l =
     let l = match l with
     | TacTerm s :: l ->
-      (** First terminal token should be considered as the name of the tactic,
-          so we tag it differently than the other terminal tokens. *)
+      (* First terminal token should be considered as the name of the tactic,
+         so we tag it differently than the other terminal tokens. *)
       primitive s :: tacarg_using_rule_token pr_gen l
     | _ -> tacarg_using_rule_token pr_gen l
     in
@@ -1180,7 +1180,7 @@ let pr_goal_selector ~toplevel s =
         pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
-        (** Those are not used by the atomic printer *)
+        (* Those are not used by the atomic printer *)
         pr_generic = (fun _ -> assert false);
         pr_extend = (fun _ _ _ -> assert false);
         pr_alias = (fun _ _ _ -> assert false);
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 06783de614..e626df5579 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -97,7 +97,7 @@ let goalevars evars = fst evars
 let cstrevars evars = snd evars
 
 let new_cstr_evar (evd,cstrs) env t =
-  (** We handle the typeclass resolution of constraints ourselves *)
+  (* We handle the typeclass resolution of constraints ourselves *)
   let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in
   let ev, _ = destEvar evd' t in
     (evd', Evar.Set.add ev cstrs), t
@@ -474,7 +474,7 @@ let get_symmetric_proof b =
 let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
 
 let rec decompose_app_rel env evd t = 
-  (** Head normalize for compatibility with the old meta mechanism *)
+  (* Head normalize for compatibility with the old meta mechanism *)
   let t = Reductionops.whd_betaiota evd t in
   match EConstr.kind evd t with
   | App (f, [||]) -> assert false
@@ -613,7 +613,7 @@ let solve_remaining_by env sigma holes by =
         Some evk
       | _ -> None
     in
-    (** Only solve independent holes *)
+    (* Only solve independent holes *)
     let indep = List.map_filter map holes in
     let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
     let solve_tac = match tac with
@@ -628,7 +628,7 @@ let solve_remaining_by env sigma holes by =
       in
       match evi with
       | None -> sigma
-        (** Evar should not be defined, but just in case *)
+        (* Evar should not be defined, but just in case *)
       | Some evi ->
         let env = Environ.reset_with_named_context evi.evar_hyps env in
         let ty = evi.evar_concl in
@@ -646,6 +646,7 @@ let poly_inverse sort =
 type rewrite_proof = 
   | RewPrf of constr * constr
   (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)
+
   | RewCast of cast_kind
   (** A proof of convertibility (with casts) *)
 
@@ -1561,7 +1562,7 @@ let newfail n s =
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
-  (** For compatibility *)
+  (* For compatibility *)
   let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
   let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
   let treat sigma res = 
@@ -1611,7 +1612,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
     let env = match clause with
     | None -> env
     | Some id ->
-      (** Only consider variables not depending on [id] *)
+      (* Only consider variables not depending on [id] *)
       let ctx = named_context env in
       let filter decl = not (occur_var_in_decl env sigma id decl) in
       let nctx = List.filter filter ctx in
@@ -1623,7 +1624,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
       in
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
       treat sigma res <*>
-      (** For compatibility *)
+      (* For compatibility *)
       beta <*> Proofview.shelve_unifiable
     with
     | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2aee809eb6..b770b97384 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -169,7 +169,7 @@ let add_tactic_entry (kn, ml, tg) state =
   let entry, pos = get_tactic_entry tg.tacgram_level in
   let mkact loc l =
     let map arg =
-      (** HACK to handle especially the tactic(...) entry *)
+      (* HACK to handle especially the tactic(...) entry *)
       let wit = Genarg.rawwit Tacarg.wit_tactic in
       if Genarg.has_type arg wit && not ml then
         Tacexp (Genarg.out_gen wit arg)
@@ -223,7 +223,7 @@ let interp_prod_item = function
       | Some arg -> arg
       end
     | Some n ->
-      (** FIXME: do better someday *)
+      (* FIXME: do better someday *)
       assert (String.equal s "tactic");
       begin match Tacarg.wit_tactic with
       | ExtraArg tag -> ArgT.Any tag
@@ -241,9 +241,9 @@ let make_fresh_key =
     | TacNonTerm _ -> "#"
     in
     let prods = String.concat "_" (List.map map prods) in
-    (** We embed the hash of the kernel name in the label so that the identifier
-        should be mostly unique. This ensures that including two modules
-        together won't confuse the corresponding labels. *)
+    (* We embed the hash of the kernel name in the label so that the identifier
+       should be mostly unique. This ensures that including two modules
+       together won't confuse the corresponding labels. *)
     let hash = (cur lxor (ModPath.hash (Lib.current_mp ()))) land 0x7FFFFFFF in
     let lbl = Id.of_string_soft (Printf.sprintf "%s_%08X" prods hash) in
     Lib.make_kn lbl
@@ -281,7 +281,7 @@ let open_tactic_notation i (_, tobj) =
 let load_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
   let () = check_key key in
-  (** Only add the printing and interpretation rules. *)
+  (* Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram);
   if Int.equal i 1 && not tobj.tacobj_local then
@@ -342,7 +342,7 @@ let extend_atomic_tactic name entries =
   let map_prod prods =
     let (hd, rem) = match prods with
     | TacTerm s :: rem -> (s, rem)
-    | _ -> assert false (** Not handled by the ML extension syntax *)
+    | _ -> assert false (* Not handled by the ML extension syntax *)
     in
     let empty_value = function
     | TacTerm s -> raise NonEmptyArgument
@@ -383,8 +383,8 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
     add_glob_tactic_notation false ~level ?deprecation prods true ids tac
   in
   List.iteri iter (List.rev prods);
-  (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
-  tactic_expr level 0) *)
+  (* We call [extend_atomic_tactic] only for "basic tactics" (the ones
+     at tactic_expr level 0) *)
   if Int.equal level 0 then extend_atomic_tactic name prods
 
 (**********************************************************************)
@@ -474,8 +474,9 @@ let register_ltac local ?deprecation tacl =
     (name, body)
   in
   let defs () =
-    (** Register locally the tactic to handle recursivity. This function affects
-        the whole environment, so that we transactify it afterwards. *)
+    (* Register locally the tactic to handle recursivity. This
+       function affects the whole environment, so that we transactify
+       it afterwards. *)
     let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in
     let () = List.iter iter_rec recvars in
     List.map map rfun
@@ -557,7 +558,7 @@ let () =
   register_grammars_by_name "tactic" entries
 
 let get_identifier i =
-  (** Workaround for badly-designed generic arguments lacking a closure *)
+  (* Workaround for badly-designed generic arguments lacking a closure *)
   Names.Id.of_string_soft (Printf.sprintf "$%i" i)
 
 type _ ty_sig =
@@ -650,20 +651,22 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
   in
   match sign with
   | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s ->
-  (** The extension is only made of a name followed by constr entries: we do not
-      add any grammar nor printing rule and add it as a true Ltac definition. *)
+    (* The extension is only made of a name followed by constr
+       entries: we do not add any grammar nor printing rule and add it
+       as a true Ltac definition. *)
     let vars = mk_sign_vars 1 s in
     let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in
     let tac = match s with
     | TyNil -> eval ml_tac
-    (** Special handling of tactics without arguments: such tactics do not do
-        a Proofview.Goal.nf_enter to compute their arguments. It matters for some
-        whole-prof tactics like [shelve_unifiable]. *)
+    (* Special handling of tactics without arguments: such tactics do
+       not do a Proofview.Goal.nf_enter to compute their arguments. It
+       matters for some whole-prof tactics like [shelve_unifiable]. *)
     | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac)
     in
-  (** Arguments are not passed directly to the ML tactic in the TacML node,
-      the ML tactic retrieves its arguments in the [ist] environment instead.
-      This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
+    (* Arguments are not passed directly to the ML tactic in the TacML
+       node, the ML tactic retrieves its arguments in the [ist]
+       environment instead.  This is the rôle of the
+       [lift_constr_tac_to_ml_tac] function. *)
     let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, [])))in
     let id = Names.Id.of_string name in
     let obj () = Tacenv.register_ltac true false id body ?deprecation in
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 2bd21f9d7a..83f563e2ab 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -78,12 +78,12 @@ type ('a,'t) match_rule =
 
 (** Extension indentifiers for the TACTIC EXTEND mechanism. *)
 type ml_tactic_name = {
+  mltac_plugin : string;
   (** Name of the plugin where the tactic is defined, typically coming from a
       DECLARE PLUGIN statement in the source. *)
-  mltac_plugin : string;
+  mltac_tactic : string;
   (** Name of the tactic entry where the tactic is defined, typically found
       after the TACTIC EXTEND statement in the source. *)
-  mltac_tactic : string;
 }
 
 type ml_tactic_entry = {
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 0c27f3bfe2..da0ecfc449 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -78,12 +78,12 @@ type ('a,'t) match_rule =
 
 (** Extension indentifiers for the TACTIC EXTEND mechanism. *)
 type ml_tactic_name = {
+  mltac_plugin : string;
   (** Name of the plugin where the tactic is defined, typically coming from a
       DECLARE PLUGIN statement in the source. *)
-  mltac_plugin : string;
+  mltac_tactic : string;
   (** Name of the tactic entry where the tactic is defined, typically found
       after the TACTIC EXTEND statement in the source. *)
-  mltac_tactic : string;
 }
 
 type ml_tactic_entry = {
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 85c6348b52..a1e21aab04 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -843,8 +843,9 @@ let notation_subst bindings tac =
     (make ?loc @@ Name id, c) :: accu
   in
   let bindings = Id.Map.fold fold bindings [] in
-  (** This is theoretically not correct due to potential variable capture, but
-      Ltac has no true variables so one cannot simply substitute *)
+  (* This is theoretically not correct due to potential variable
+     capture, but Ltac has no true variables so one cannot simply
+     substitute *)
   TacLetIn (false, bindings, tac)
 
 let () = Genintern.register_ntn_subst0 wit_tactic notation_subst
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index cf5eb442be..284642b38c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -50,7 +50,7 @@ let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v w
   let Val.Dyn (t, _) = v in
   let t' = match val_tag wit with
   | Val.Base t' -> t'
-  | _ -> assert false (** not used in this module *)
+  | _ -> assert false (* not used in this module *)
   in
   match Val.eq t t' with
   | None -> false
@@ -68,13 +68,13 @@ let in_list tag v =
 let in_gen wit v =
   let t = match val_tag wit with
   | Val.Base t -> t
-  | _ -> assert false (** not used in this module *)
+  | _ -> assert false (* not used in this module *)
   in
   Val.Dyn (t, v)
 let out_gen wit v =
   let t = match val_tag wit with
   | Val.Base t -> t
-  | _ -> assert false (** not used in this module *)
+  | _ -> assert false (* not used in this module *)
   in
   match prj t v with None -> assert false | Some x -> x
 
@@ -585,8 +585,8 @@ let interp_pure_open_constr ist =
 let interp_typed_pattern ist env sigma (_,c,_) =
   let sigma, c =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
-  (** FIXME: it is necessary to be unsafe here because of the way we handle
-      evars in the pretyper. Sometimes they get solved eagerly. *)
+  (* FIXME: it is necessary to be unsafe here because of the way we handle
+     evars in the pretyper. Sometimes they get solved eagerly. *)
   pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
 
 (* Interprets a constr expression *)
@@ -897,7 +897,7 @@ let interp_destruction_arg ist gl arg =
           end)
       in
       try
-        (** FIXME: should be moved to taccoerce *)
+        (* FIXME: should be moved to taccoerce *)
         let v = Id.Map.find id ist.lfun in
         if has_type v (topwit wit_intro_pattern) then
           let v = out_gen (topwit wit_intro_pattern) v in
@@ -1020,7 +1020,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
   | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr
   | TacArg {loc;v} -> interp_tacarg ist v
   | t ->
-    (** Delayed evaluation *)
+    (* Delayed evaluation *)
     Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t)))
   in
   let open Ftactic in
@@ -1396,12 +1396,12 @@ and interp_match_successes lz ist s =
         general
     | Select ->
       begin
-        (** Only keep the first matching result, we don't backtrack on it *)
+        (* Only keep the first matching result, we don't backtrack on it *)
         let s = Proofview.tclONCE s in
         s >>= fun ans -> interp_match_success ist ans
       end
     | Once ->
-        (** Once a tactic has succeeded, do not backtrack anymore *)
+        (* Once a tactic has succeeded, do not backtrack anymore *)
         Proofview.tclONCE general
 
 (* Interprets the Match expressions *)
@@ -1438,7 +1438,7 @@ and interp_match_goal ist lz lr lmr =
 (* Interprets extended tactic generic arguments *)
 and interp_genarg ist x : Val.t Ftactic.t =
     let open Ftactic.Notations in
-    (** Ad-hoc handling of some types. *)
+    (* Ad-hoc handling of some types. *)
     let tag = genarg_tag x in
     if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then
       interp_genarg_var_list ist x
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index c949589e22..54924f1644 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -59,7 +59,7 @@ let id_map_try_add_name id x m =
     the binding of the right-hand argument shadows that of the left-hand
     argument. *)
 let id_map_right_biased_union m1 m2 =
-  if Id.Map.is_empty m1 then m2 (** Don't reconstruct the whole map *)
+  if Id.Map.is_empty m1 then m2 (* Don't reconstruct the whole map *)
   else Id.Map.fold Id.Map.add m2 m1
 
 (** Tests whether the substitution [s] is empty. *)
@@ -102,7 +102,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
         else raise Not_coherent_metas
   in
   let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 in
-  (** ppedrot: Is that even correct? *)
+  (* ppedrot: Is that even correct? *)
   let merged = ln +++ ln1 in
   (merged, Id.Map.merge merge lcm lm)
 
@@ -263,8 +263,8 @@ module PatternMatching (E:StaticEnvironment) = struct
     | All lhs -> wildcard_match_term lhs
     | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs
     | Pat _ ->
-        (** Rules with hypotheses, only work in match goal. *)
-        fail
+      (* Rules with hypotheses, only work in match goal. *)
+      fail
 
   (** [match_term term rules] matches the term [term] with the set of
       matching rules [rules].*)