Merge PR #10337: [stm] [vernac] Remove special ?proof parameter from vernac main path

Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares

3 files changed, 6 insertions, 6 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index a904b81d81..f773b2c39e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1005,7 +1005,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       lemma_type
   in
   let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
-  let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
+  let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
   evd
 
 let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 587e1fc2e8..86defb2f2f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -815,7 +815,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lemma = fst @@ Lemmas.by
                    (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
                                                       (proving_tac i))) lemma in
-         let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
+         let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
          let finfo = find_Function_infos (fst f_as_constant) in
          (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
          let _,lem_cst_constr = Evd.fresh_global
@@ -877,7 +877,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lemma = fst (Lemmas.by
                             (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
                                                      (proving_tac i))) lemma) in
-         let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
+         let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
          let finfo = find_Function_infos (fst f_as_constant) in
          let _,lem_cst_constr = Evd.fresh_global
                                   (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 425e498330..b68b31c93b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -71,7 +71,7 @@ let declare_fun f_id kind ?univs value =
     ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
 let defined lemma =
-  Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None
+  Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
 
 let def_of_const t =
    match (Constr.kind t) with
@@ -1365,7 +1365,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
                )
                  g)
     in
-    Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
+    Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma)
@@ -1492,7 +1492,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
                }
           )
        )) lemma in
-    let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None) () in
+    let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None) () in
     ()
 (*      Pp.msgnl (fun _ _ -> str "eqn finished"); *)