[stm] [vernac] Remove special ?proof parameter from vernac main path

We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.

This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.

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