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

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

11 files changed, 189 insertions, 170 deletions

diff --git a/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh b/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh
new file mode 100644
index 0000000000..288e14c866
--- /dev/null
+++ b/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10337" ] || [ "$CI_BRANCH" = "vernac+qed_special_case_inject_proof" ]; then
+
+    paramcoq_CI_REF=vernac+qed_special_case_inject_proof
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    equations_CI_REF=vernac+qed_special_case_inject_proof
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
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"); *)
 
diff --git a/stm/stm.ml b/stm/stm.ml
index f3ae32a719..91397950f6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1060,10 +1060,19 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
+(* Wrapper for the proof-closing special path for Qed *)
+let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc pending : Vernacstate.t =
+  set_id_for_feedback ?route dummy_doc id;
+  try
+    Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc pending
+  with e ->
+    let e = CErrors.push e in
+    Exninfo.iraise Hooks.(call_process_error_once e)
+
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 (* It is currently called 19 times, this number should be certainly
    reduced... *)
-let stm_vernac_interp ?proof ?route id st { verbose; expr } : Vernacstate.t =
+let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t =
   (* The Stm will gain the capability to interpret commmads affecting
      the whole document state, such as backtrack, etc... so we start
      to design the stm command interpreter now *)
@@ -1085,7 +1094,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; expr } : Vernacstate.t =
     (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
   else begin
     stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
-    try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr
+    try Vernacentries.interp ?verbosely:(Some verbose) ~st expr
     with e ->
       let e = CErrors.push e in
       Exninfo.iraise Hooks.(call_process_error_once e)
@@ -1536,10 +1545,8 @@ end = struct (* {{{ *)
             PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
-          stm_vernac_interp stop
-            ~proof:(pobject, Lemmas.Info.make ()) st
-            { verbose = false; indentation = 0; strlen = 0;
-              expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
+          stm_qed_delay_proof ~st ~id:stop
+            ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc (Proved (opaque,None))) in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1674,10 +1681,10 @@ end = struct (* {{{ *)
       let opaque = Proof_global.Opaque in
 
       (* The original terminator, a hook, has not been saved in the .vio*)
-      let pterm, _info =
+      let proof, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
 
-      let proof = pterm, Lemmas.Info.make () in
+      let info = Lemmas.Info.make () in
 
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
@@ -1690,9 +1697,7 @@ end = struct (* {{{ *)
        *)
       (* STATE We use the state resulting from reaching start. *)
       let st = Vernacstate.freeze_interp_state ~marshallable:false in
-      ignore(stm_vernac_interp stop ~proof st
-        { verbose = false; indentation = 0; strlen = 0;
-          expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
+      ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc (Proved (opaque,None)));
       `OK proof
       end
     with e ->
@@ -1732,10 +1737,8 @@ end = struct (* {{{ *)
     | `ERROR -> exit 1
     | `ERROR_ADMITTED -> cst, false
     | `OK_ADMITTED -> cst, false
-    | `OK (po,_) ->
-        let con =
-          Nametab.locate_constant
-            (Libnames.qualid_of_ident po.Proof_global.name) in
+    | `OK { Proof_global.name } ->
+        let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in
         let c = Global.lookup_constant con in
         let o = match c.Declarations.const_body with
           | Declarations.OpaqueDef o -> o
@@ -2357,6 +2360,14 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
       try f x
       with e when CErrors.noncritical e -> () in
 
+  (* extract proof_ending in qed case, note that `Abort` and `Proof
+     term.` could also fail in this case, however that'd be a bug I do
+     believe as proof injection shouldn't happen here. *)
+  let extract_pe (x : aast) =
+    match Vernacprop.under_control x.expr with
+    | VernacEndProof pe -> pe
+    | _ -> CErrors.anomaly Pp.(str "Non-qed command classified incorrectly") in
+
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
   let cherry_pick_non_pstate () =
@@ -2485,12 +2496,12 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                         Proof_global.Opaque (* Admitted -> Opaque should be OK. *)
                       | VtKeepDefined -> Proof_global.Transparent
                     in
-                    let proof =
+                    let proof, info =
                       PG_compat.close_future_proof ~opaque ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     let st = Vernacstate.freeze_interp_state ~marshallable:false in
-                    ignore(stm_vernac_interp id ~proof st x);
+                    ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x));
                     feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
@@ -2506,7 +2517,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 log_processing_sync id name reason;
                 reach eop;
                 let wall_clock = Unix.gettimeofday () in
-                record_pb_time name ?loc:x.expr.CAst.loc (wall_clock -. !wall_clock_last_fork);
+                let loc = x.expr.CAst.loc in
+                record_pb_time name ?loc (wall_clock -. !wall_clock_last_fork);
                 let proof =
                   match keep with
                   | VtDrop -> None
@@ -2526,7 +2538,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                   reach view.next;
                 let wall_clock2 = Unix.gettimeofday () in
                 let st = Vernacstate.freeze_interp_state ~marshallable:false in
-                ignore(stm_vernac_interp id ?proof st x);
+                let _st = match proof with
+                  | None ->  stm_vernac_interp id st x
+                  | Some (proof, info) ->
+                    stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x)
+                in
                 let wall_clock3 = Unix.gettimeofday () in
                 Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
                   (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 81cde786c2..759e907bc9 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -497,7 +497,7 @@ type obligation_qed_info =
   ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress
   }
 
-let obligation_terminator opq entries uctx { name; num; auto } =
+let obligation_terminator entries uctx { name; num; auto } =
   let open Proof_global in
   match entries with
   | [entry] ->
@@ -517,13 +517,13 @@ let obligation_terminator opq entries uctx { name; num; auto } =
     let obls, rem = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
-      match obl.obl_status, opq with
-      | (_, Evar_kinds.Expand), Opaque -> err_not_transp ()
-      | (true, _), Opaque -> err_not_transp ()
-      | (false, _), Opaque -> Evar_kinds.Define true
-      | (_, Evar_kinds.Define true), Transparent ->
+      match obl.obl_status, entry.proof_entry_opaque with
+      | (_, Evar_kinds.Expand), true -> err_not_transp ()
+      | (true, _), true -> err_not_transp ()
+      | (false, _), true -> Evar_kinds.Define true
+      | (_, Evar_kinds.Define true), false ->
         Evar_kinds.Define false
-      | (_, status), Transparent -> status
+      | (_, status), false -> status
     in
     let obl = { obl with obl_status = false, status } in
     let ctx =
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 2d275b5ed8..fae27e1cb3 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -79,8 +79,7 @@ type obligation_qed_info =
   }
 
 val obligation_terminator
-  :  Proof_global.opacity_flag
-  -> Evd.side_effects Proof_global.proof_entry list
+  : Evd.side_effects Proof_global.proof_entry list
   -> UState.t
   -> obligation_qed_info -> unit
 (** [obligation_terminator] part 2 of saving an obligation *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 35b902fff9..31407de4da 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -455,69 +455,42 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
   process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms;
   Feedback.feedback Feedback.AddedAxiom
 
-let save_lemma_admitted ?proof ~(lemma : t) =
-    let open Proof_global in
-    let env = Global.env () in
-    match proof with
-    | Some ({ name; entries; universes; udecl }, { Info.hook; scope; impargs; other_thms; _} ) ->
-      if List.length entries <> 1 then
-        user_err Pp.(str "Admitted does not support multiple statements");
-      let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
-      if proof_entry_type = None then
-        user_err Pp.(str "Admitted requires an explicit statement");
-      let poly = match proof_entry_universes with
-        | Entries.Monomorphic_entry _ -> false
-        | Entries.Polymorphic_entry (_, _) -> true in
-      let typ = Option.get proof_entry_type in
-      let ctx = UState.univ_entry ~poly universes in
-      let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-      let sigma = Evd.from_env env in
-      finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
-    | None ->
-      let pftree = Proof_global.get_proof lemma.proof in
-      let scope = lemma.info.Info.scope in
-      let Proof.{ name; poly; entry } = Proof.data pftree in
-      let typ = match Proofview.initial_goals entry with
-        | [typ] -> snd typ
-        | _ ->
-          CErrors.anomaly
-            ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
-      in
-      let typ = EConstr.Unsafe.to_constr typ in
-      let universes = Proof_global.get_initial_euctx lemma.proof in
-      (* This will warn if the proof is complete *)
-      let pproofs, _univs =
-        Proof_global.return_proof ~allow_partial:true lemma.proof in
-      let sec_vars =
-        if not (get_keep_admitted_vars ()) then None
-        else match Proof_global.get_used_variables lemma.proof, pproofs with
-          | Some _ as x, _ -> x
-          | None, (pproof, _) :: _ ->
-            let env = Global.env () in
-            let ids_typ = Environ.global_vars_set env typ in
-            let ids_def = Environ.global_vars_set env pproof in
-            Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
-          | _ -> None in
-      let udecl = Proof_global.get_universe_decl lemma.proof in
-      let { Info.hook; impargs; other_thms } = lemma.info in
-      let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
-      let ctx = UState.check_univ_decl ~poly universes udecl in
-      finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+let save_lemma_admitted ~(lemma : t) : unit =
+  (* Used for printing in recthms *)
+  let env = Global.env () in
+  let { Info.hook; scope; impargs; other_thms } = lemma.info in
+  let udecl = Proof_global.get_universe_decl lemma.proof in
+  let Proof.{ sigma; name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
+  let typ = match Proofview.initial_goals entry with
+    | [typ] -> snd typ
+    | _ -> CErrors.anomaly ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
+  in
+  let typ = EConstr.Unsafe.to_constr typ in
+  (* This will warn if the proof is complete *)
+  let pproofs, _univs = Proof_global.return_proof ~allow_partial:true lemma.proof in
+  let sec_vars =
+    if not (get_keep_admitted_vars ()) then None
+    else match Proof_global.get_used_variables lemma.proof, pproofs with
+      | Some _ as x, _ -> x
+      | None, (pproof, _) :: _ ->
+        let env = Global.env () in
+        let ids_typ = Environ.global_vars_set env typ in
+        let ids_def = Environ.global_vars_set env pproof in
+        Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
+      | _ -> None in
+  let universes = Proof_global.get_initial_euctx lemma.proof in
+  let ctx = UState.check_univ_decl ~poly universes udecl in
+  finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
 (************************************************************************)
 
-let finish_proved env sigma opaque idopt po info =
+let finish_proved env sigma idopt po info =
   let open Proof_global in
   let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in
   match po with
   | { name; entries=[const]; universes; udecl; poly } ->
-    let is_opaque = match opaque with
-      | Transparent -> false
-      | Opaque      -> true
-    in
-    assert (is_opaque == const.proof_entry_opaque);
     let name = match idopt with
       | None -> name
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
@@ -555,16 +528,16 @@ let finish_proved env sigma opaque idopt po info =
   | _ ->
     CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term")
 
-let finish_derived ~f ~name ~idopt ~opaque ~entries =
+let finish_derived ~f ~name ~idopt ~entries =
   (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *)
 
   if Option.has_some idopt then
     CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.");
 
-  let opaque, f_def, lemma_def =
+  let f_def, lemma_def =
     match entries with
     | [_;f_def;lemma_def] ->
-      opaque <> Proof_global.Transparent , f_def , lemma_def
+      f_def, lemma_def
     | _ -> assert false
   in
   (* The opacity of [f_def] is adjusted to be [false], as it
@@ -590,17 +563,17 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
   let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
   let lemma_def = let open Proof_global in
     { lemma_def with
-      proof_entry_body = lemma_body ;
-      proof_entry_type = Some lemma_type ;
-      proof_entry_opaque = opaque ; }
+      proof_entry_body = lemma_body;
+      proof_entry_type = Some lemma_type }
   in
   let lemma_def =
     Declare.DefinitionEntry lemma_def ,
     Decl_kinds.(IsProof Proposition)
   in
-  ignore (Declare.declare_constant name lemma_def)
+  let _ : Names.Constant.t = Declare.declare_constant name lemma_def in
+  ()
 
-let finish_proved_equations opaque lid kind proof_obj hook i types wits sigma0 =
+let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
 
   let open Decl_kinds in
   let obls = ref 1 in
@@ -624,32 +597,50 @@ let finish_proved_equations opaque lid kind proof_obj hook i types wits sigma0 =
   in
   hook recobls sigma
 
-let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
-  (* Invariant (uh) *)
-  if Option.is_empty lemma && Option.is_empty proof then
-    user_err (str "No focused proof (No proof-editing in progress).");
-  (* Env and sigma are just used for error printing in save_remaining_recthms *)
-  let env = Global.env () in
-  let sigma, proof_obj, proof_info =
-    match proof with
-    | None ->
-      (* XXX: The close_proof and proof state API should be refactored
-         so it is possible to insert proofs properly into the state *)
-      let { proof; info } = Option.get lemma in
-      let { Proof.sigma } = Proof.data (Proof_global.get_proof proof) in
-      sigma,
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, info
-    | Some (proof, info) ->
-      Evd.from_env env, proof, info
-  in
+let finalize_proof idopt env sigma proof_obj proof_info =
   let open Proof_global in
   let open Proof_ending in
   match CEphemeron.default proof_info.Info.proof_ending Regular with
   | Regular ->
-    finish_proved env sigma opaque idopt proof_obj proof_info
+    finish_proved env sigma idopt proof_obj proof_info
   | End_obligation oinfo ->
-    DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo
+    DeclareObl.obligation_terminator proof_obj.entries proof_obj.universes oinfo
   | End_derive { f ; name } ->
-    finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries
+    finish_derived ~f ~name ~idopt ~entries:proof_obj.entries
   | End_equations { hook; i; types; wits; sigma } ->
-    finish_proved_equations opaque idopt proof_info.Info.kind proof_obj hook i types wits sigma
+    finish_proved_equations idopt proof_info.Info.kind proof_obj hook i types wits sigma
+
+let save_lemma_proved ~lemma ~opaque ~idopt =
+  (* Env and sigma are just used for error printing in save_remaining_recthms *)
+  let env = Global.env () in
+  let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
+  let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in
+  finalize_proof idopt env sigma proof_obj lemma.info
+
+(***********************************************************************)
+(* Special case to close a lemma without forcing a proof               *)
+(***********************************************************************)
+let save_lemma_admitted_delayed ~proof ~info =
+  let open Proof_global in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let { name; entries; universes; udecl; poly } = proof in
+  let { Info.hook; scope; impargs; other_thms } = info in
+  if List.length entries <> 1 then
+    user_err Pp.(str "Admitted does not support multiple statements");
+  let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
+  let poly = match proof_entry_universes with
+    | Entries.Monomorphic_entry _ -> false
+    | Entries.Polymorphic_entry (_, _) -> true in
+  let typ = match proof_entry_type with
+    | None -> user_err Pp.(str "Admitted requires an explicit statement");
+    | Some typ -> typ in
+  let ctx = UState.univ_entry ~poly universes in
+  let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
+  finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+
+let save_lemma_proved_delayed ~proof ~info ~idopt =
+  (* Env and sigma are just used for error printing in save_remaining_recthms *)
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  finalize_proof idopt env sigma proof info
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 276d7ae144..d156954c85 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -129,21 +129,9 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** {4 Saving proofs} *)
 
-(** The extra [?proof] parameter here is due to problems with the
-    lower-level [Proof_global.close_proof] API; we cannot inject closed
-    proofs properly in the proof state so we must leave this backdoor open.
-
-    The regular user can ignore it.
-*)
-
-val save_lemma_admitted
-  :  ?proof:(Proof_global.proof_object * Info.t)
-  -> lemma:t
-  -> unit
-
+val save_lemma_admitted : lemma:t -> unit
 val save_lemma_proved
-  :  ?proof:(Proof_global.proof_object * Info.t)
-  -> ?lemma:t
+  :  lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> unit
@@ -153,3 +141,12 @@ module Internal : sig
   val get_info : t -> Info.t
   (** Only needed due to the Proof_global compatibility layer. *)
 end
+
+(** Special cases for delayed proofs, in this case we must provide the
+   proof information so the proof won't be forced. *)
+val save_lemma_admitted_delayed : proof:Proof_global.proof_object -> info:Info.t -> unit
+val save_lemma_proved_delayed
+  :  proof:Proof_global.proof_object
+  -> info:Info.t
+  -> idopt:Names.lident option
+  -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2bcd06b4d9..e0183b941e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -47,16 +47,6 @@ let vernac_pperr_endline pp =
    instead enviroment/state selection should be done at the Vernac DSL
    level. *)
 
-(* EJGA: Only used in close_proof, can remove once the ?proof hack is no more *)
-let vernac_require_open_lemma ~stack f =
-  match stack with
-  | Some stack -> f ~stack
-  | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
-
-let with_pstate ~stack f =
-  vernac_require_open_lemma ~stack
-    (fun ~stack -> Vernacstate.LemmaStack.with_top_pstate stack ~f:(fun pstate -> f ~pstate))
-
 let get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
@@ -642,27 +632,17 @@ let vernac_start_proof ~atts kind l =
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
   start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Proof kind) l
 
-let vernac_end_proof ?stack ?proof = let open Vernacexpr in function
+let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
-    vernac_require_open_lemma ~stack (fun ~stack ->
-      let lemma, stack = Vernacstate.LemmaStack.pop stack in
-      save_lemma_admitted ?proof ~lemma;
-      stack)
+    save_lemma_admitted ~lemma
   | Proved (opaque,idopt) ->
-    let lemma, stack = match stack with
-      | None -> None, None
-      | Some stack ->
-        let lemma, stack = Vernacstate.LemmaStack.pop stack in
-        Some lemma, stack
-    in
-    save_lemma_proved ?lemma ?proof ~opaque ~idopt;
-    stack
+    save_lemma_proved ~lemma ~opaque ~idopt
 
 let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
   let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in
-  let () = save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
+  let () = save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -2324,6 +2304,12 @@ let locate_if_not_already ?loc (e, info) =
 
 exception End_of_input
 
+(* EJGA: We may remove this, only used twice below *)
+let vernac_require_open_lemma ~stack f =
+  match stack with
+  | Some stack -> f stack
+  | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
+
 let interp_typed_vernac c ~stack =
   let open Vernacextend in
   match c with
@@ -2334,7 +2320,7 @@ let interp_typed_vernac c ~stack =
     let () = f () in
     stack
   | VtCloseProof f ->
-    vernac_require_open_lemma ~stack (fun ~stack ->
+    vernac_require_open_lemma ~stack (fun stack ->
         let lemma, stack = Vernacstate.LemmaStack.pop stack in
         f ~lemma;
         stack)
@@ -2347,13 +2333,13 @@ let interp_typed_vernac c ~stack =
     f ~pstate;
     stack
   | VtReadProof f ->
-    with_pstate ~stack f;
+    vernac_require_open_lemma ~stack
+      (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate));
     stack
 
 (* We interpret vernacular commands to a DSL that specifies their
    allowed actions on proof states *)
 let translate_vernac ~atts v = let open Vernacextend in match v with
-  | VernacEndProof _
   | VernacAbortAll
   | VernacRestart
   | VernacUndo _
@@ -2664,6 +2650,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacProofMode mn ->
     VtDefault(fun () -> unsupported_attributes atts)
 
+  | VernacEndProof pe ->
+    VtCloseProof (vernac_end_proof pe)
+
   (* Extensions *)
   | VernacExtend (opn,args) ->
     Vernacextend.type_vernac ~atts opn args
@@ -2698,11 +2687,6 @@ let rec interp_expr ?proof ~atts ~st c =
     unsupported_attributes atts;
     vernac_load ~verbosely ~st fname
 
-  (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *)
-  | VernacEndProof e ->
-    unsupported_attributes atts;
-    vernac_end_proof ?proof ?stack e
-
   | v ->
     let fv = translate_vernac ~atts v in
     interp_typed_vernac ~stack fv
@@ -2773,11 +2757,11 @@ let () =
       optwrite = ((:=) default_timeout) }
 
 (* Be careful with the cache here in case of an exception. *)
-let interp ?(verbosely=true) ?proof ~st cmd =
+let interp ?(verbosely=true) ~st cmd =
   Vernacstate.unfreeze_interp_state st;
   try vernac_timeout (fun st ->
       let v_mod = if verbosely then Flags.verbosely else Flags.silently in
-      let ontop = v_mod (interp_control ?proof ~st) cmd in
+      let ontop = v_mod (interp_control ~st) cmd in
       Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
       Vernacstate.freeze_interp_state ~marshallable:false
     ) st
@@ -2786,3 +2770,19 @@ let interp ?(verbosely=true) ?proof ~st cmd =
     let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
     Vernacstate.invalidate_cache ();
     iraise exn
+
+let interp_qed_delayed_proof ~proof ~info ~st ?loc pe : Vernacstate.t =
+  let stack = st.Vernacstate.lemmas in
+  let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
+  try
+    let () = match pe with
+      | Admitted ->
+        save_lemma_admitted_delayed ~proof ~info
+      | Proved (_,idopt) ->
+        save_lemma_proved_delayed ~proof ~info ~idopt in
+    { st with Vernacstate.lemmas = stack }
+  with exn ->
+    let exn = CErrors.push exn in
+    let exn = locate_if_not_already ?loc exn in
+    Vernacstate.invalidate_cache ();
+    iraise exn
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index ad3e9f93d9..3563e9984a 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -20,10 +20,17 @@ val vernac_require :
   Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
 
 (** The main interpretation function of vernacular expressions *)
-val interp :
-  ?verbosely:bool ->
-  ?proof:(Proof_global.proof_object * Lemmas.Info.t) ->
-  st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
+val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
+
+(** Execute a Qed but with a proof_object which may contain a delayed
+   proof and won't be forced *)
+val interp_qed_delayed_proof
+  :  proof:Proof_global.proof_object
+  -> info:Lemmas.Info.t
+  -> st:Vernacstate.t
+  -> ?loc:Loc.t
+  -> Vernacexpr.proof_end
+  -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name