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

7 files changed, 55 insertions, 55 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index b7ccd647b5..1f1bdf4da7 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -601,17 +601,17 @@ let make_evar_clause env sigma ?len t =
   | None -> -1
   | Some n -> assert (0 <= n); n
   in
-  (** FIXME: do the renaming online *)
+  (* FIXME: do the renaming online *)
   let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
   let rec clrec (sigma, holes) inst n t =
     if n = 0 then (sigma, holes, t)
     else match EConstr.kind sigma t with
     | Cast (t, _, _) -> clrec (sigma, holes) inst n t
     | Prod (na, t1, t2) ->
-      (** Share the evar instances as we are living in the same context *)
+      (* Share the evar instances as we are living in the same context *)
       let inst, ctx, args, subst = match inst with
       | None ->
-        (** Dummy type *)
+        (* Dummy type *)
         let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in
         Some (ctx, args, subst), ctx, args, subst
       | Some (ctx, args, subst) -> inst, ctx, args, subst
@@ -688,7 +688,7 @@ let solve_evar_clause env sigma hyp_only clause = function
   let open EConstr in
   let fold holes h =
     if h.hole_deps then
-      (** Some subsequent term uses the hole *)
+      (* Some subsequent term uses the hole *)
       let (ev, _) = destEvar sigma h.hole_evar in
       let is_dep hole = occur_evar sigma ev hole.hole_type in
       let in_hyp = List.exists is_dep holes in
@@ -697,7 +697,7 @@ let solve_evar_clause env sigma hyp_only clause = function
       let h = { h with hole_deps = dep } in
       h :: holes
     else
-      (** The hole does not occur anywhere *)
+      (* The hole does not occur anywhere *)
       h :: holes
   in
   let holes = List.fold_left fold [] (List.rev clause.cl_holes) in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 4720328893..c36b0fa337 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -61,9 +61,9 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
   clenv_pose_metas_as_evars clenv dep_mvs
 
 let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
-  (** ppedrot: a Goal.enter here breaks things, because the tactic below may
-      solve goals by side effects, while the compatibility layer keeps those
-      useless goals. That deserves a FIXME. *)
+  (* ppedrot: a Goal.enter here breaks things, because the tactic below may
+     solve goals by side effects, while the compatibility layer keeps those
+     useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
   let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 15ba0a704f..456ab879eb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -373,8 +373,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	check_typability env sigma ty;
         let sigma = check_conv_leq_goal env sigma trm ty conclty in
 	let res = mk_refgoals sigma goal goalacc ty t in
-	(** we keep the casts (in particular VMcast and NATIVEcast) except
-	    when they are annotating metas *)
+        (* we keep the casts (in particular VMcast and NATIVEcast) except
+           when they are annotating metas *)
 	if isMeta t then begin
 	  assert (k != VMcast && k != NATIVEcast);
 	  res
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 886a62cb89..acf5510aa0 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -167,23 +167,23 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   cb, status, univs
 
 let refine_by_tactic env sigma ty tac =
-  (** Save the initial side-effects to restore them afterwards. We set the
-      current set of side-effects to be empty so that we can retrieve the
-      ones created during the tactic invocation easily. *)
+  (* Save the initial side-effects to restore them afterwards. We set the
+     current set of side-effects to be empty so that we can retrieve the
+     ones created during the tactic invocation easily. *)
   let eff = Evd.eval_side_effects sigma in
   let sigma = Evd.drop_side_effects sigma in
-  (** Save the existing goals *)
+  (* Save the existing goals *)
   let prev_future_goals = save_future_goals sigma in
-  (** Start a proof *)
+  (* Start a proof *)
   let prf = Proof.start sigma [env, ty] in
   let (prf, _) =
     try Proof.run_tactic env tac prf
     with Logic_monad.TacticFailure e as src ->
-      (** Catch the inner error of the monad tactic *)
+      (* Catch the inner error of the monad tactic *)
       let (_, info) = CErrors.push src in
       iraise (e, info)
   in
-  (** Plug back the retrieved sigma *)
+  (* Plug back the retrieved sigma *)
   let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in
   assert (stack = []);
   let ans = match Proof.initial_goals prf with
@@ -191,26 +191,26 @@ let refine_by_tactic env sigma ty tac =
   | _ -> assert false
   in
   let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
-  (** [neff] contains the freshly generated side-effects *)
+  (* [neff] contains the freshly generated side-effects *)
   let neff = Evd.eval_side_effects sigma in
-  (** Reset the old side-effects *)
+  (* Reset the old side-effects *)
   let sigma = Evd.drop_side_effects sigma in
   let sigma = Evd.emit_side_effects eff sigma in
-  (** Restore former goals *)
+  (* Restore former goals *)
   let sigma = restore_future_goals sigma prev_future_goals in
-  (** Push remaining goals as future_goals which is the only way we
-      have to inform the caller that there are goals to collect while
-      not being encapsulated in the monad *)
-  (** Goals produced by tactic "shelve" *)
+  (* Push remaining goals as future_goals which is the only way we
+     have to inform the caller that there are goals to collect while
+     not being encapsulated in the monad *)
+  (* Goals produced by tactic "shelve" *)
   let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
-  (** Goals produced by tactic "give_up" *)
+  (* Goals produced by tactic "give_up" *)
   let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
-  (** Other goals *)
+  (* Other goals *)
   let sigma = List.fold_right Evd.declare_future_goal goals sigma in
-  (** Get rid of the fresh side-effects by internalizing them in the term
-      itself. Note that this is unsound, because the tactic may have solved
-      other goals that were already present during its invocation, so that
-      those goals rely on effects that are not present anymore. Hopefully,
-      this hack will work in most cases. *)
+  (* Get rid of the fresh side-effects by internalizing them in the term
+     itself. Note that this is unsound, because the tactic may have solved
+     other goals that were already present during its invocation, so that
+     those goals rely on effects that are not present anymore. Hopefully,
+     this hack will work in most cases. *)
   let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
   ans, sigma
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 67e19df0e7..76a1e61ad2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -422,9 +422,9 @@ let return_proof ?(allow_partial=false) () =
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in
   let eff = Evd.eval_side_effects evd in
-  (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-      side-effects... This may explain why one need to uniquize side-effects
-      thereafter... *)
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
   let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
     proofs, Evd.evar_universe_context evd
  end else
@@ -432,9 +432,9 @@ let return_proof ?(allow_partial=false) () =
   let evd = Proof.return ~pid proof in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.minimize_universes evd in
-  (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-      side-effects... This may explain why one need to uniquize side-effects
-      thereafter... *)
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
   let proofs =
     List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 540a8bb420..d812a8cad7 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -27,7 +27,7 @@ let extract_prefix env info =
 
 let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
-  (** Typecheck the hypotheses. *)
+  (* Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
     let t = NamedDecl.get_type decl in
     let sigma, _ = Typing.sort_of env sigma t in
@@ -40,7 +40,7 @@ let typecheck_evar ev env sigma =
   let (common, changed) = extract_prefix env info in
   let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
-  (** Typecheck the conclusion *)
+  (* Typecheck the conclusion *)
   let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
   sigma
 
@@ -60,39 +60,39 @@ let generic_refine ~typecheck f gl =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   let state = Proofview.Goal.state gl in
-  (** Save the [future_goals] state to restore them after the
-      refinement. *)
+  (* Save the [future_goals] state to restore them after the
+     refinement. *)
   let prev_future_goals = Evd.save_future_goals sigma in
-  (** Create the refinement term *)
+  (* Create the refinement term *)
   Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
   f >>= fun (v, c) ->
   Proofview.tclEVARMAP >>= fun sigma ->
   Proofview.V82.wrap_exceptions begin fun () ->
   let evs = Evd.save_future_goals sigma in
-  (** Redo the effects in sigma in the monad's env *)
+  (* Redo the effects in sigma in the monad's env *)
   let privates_csts = Evd.eval_side_effects sigma in
   let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
   let env = add_side_effects env sideff in
-  (** Check that the introduced evars are well-typed *)
+  (* Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
-  (** Check that the refined term is typesafe *)
+  (* Check that the refined term is typesafe *)
   let sigma = if typecheck then Typing.check env sigma c concl else sigma in
-  (** Check that the goal itself does not appear in the refined term *)
+  (* Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
     if not (Evarutil.occur_evar_upto sigma self c) then ()
     else Pretype_errors.error_occur_check env sigma self c
   in
-  (** Restore the [future goals] state. *)
+  (* Restore the [future goals] state. *)
   let sigma = Evd.restore_future_goals sigma prev_future_goals in
-  (** Select the goals *)
+  (* Select the goals *)
   let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
   let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
-  (** Proceed to the refinement *)
+  (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
-    (** Nothing to do, the goal has been solved by side-effect *)
+    (* Nothing to do, the goal has been solved by side-effect *)
     sigma
   | Some self ->
     match evkmain with
@@ -104,7 +104,7 @@ let generic_refine ~typecheck f gl =
         | None -> sigma
         | Some id -> Evd.rename evk id sigma
   in
-  (** Mark goals *)
+  (* Mark goals *)
   let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
   let trace () = Pp.(hov 2 (str"simple refine"++spc()++
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 64d7630d55..a5f691babb 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -133,7 +133,7 @@ module New = struct
     f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
   let pf_global id gl =
-    (** We only check for the existence of an [id] in [hyps] *)
+    (* We only check for the existence of an [id] in [hyps] *)
     let hyps = Proofview.Goal.hyps gl in
     Constrintern.construct_reference hyps id
 
@@ -149,12 +149,12 @@ module New = struct
   let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
 
   let pf_ids_of_hyps gl =
-    (** We only get the identifiers in [hyps] *)
+    (* We only get the identifiers in [hyps] *)
     let hyps = Proofview.Goal.hyps gl in
     ids_of_named_context hyps
 
   let pf_ids_set_of_hyps gl =
-    (** We only get the identifiers in [hyps] *)
+    (* We only get the identifiers in [hyps] *)
     let env = Proofview.Goal.env gl in
     Environ.ids_of_named_context_val (Environ.named_context_val env)
 
@@ -186,7 +186,7 @@ module New = struct
     List.hd hyps
 
   let pf_nf_concl (gl : Proofview.Goal.t) =
-    (** We normalize the conclusion just after *)
+    (* We normalize the conclusion just after *)
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
     nf_evar sigma concl