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

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

1 files changed, 3 insertions, 3 deletions

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"); *)