[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.

4 files changed, 121 insertions, 119 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 35b902fff9..bfd7e6b495 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -455,54 +455,32 @@ 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                                         *)
@@ -598,7 +576,8 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
     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 =
 
@@ -624,24 +603,7 @@ 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 opaque proof_obj proof_info =
   let open Proof_global in
   let open Proof_ending in
   match CEphemeron.default proof_info.Info.proof_ending Regular with
@@ -653,3 +615,38 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
     finish_derived ~f ~name ~idopt ~opaque ~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
+
+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 opaque 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 ~opaque ~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 opaque proof info
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 276d7ae144..733d84d676 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,13 @@ 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
+  -> opaque:Proof_global.opacity_flag
+  -> idopt:Names.lident option
+  -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2bcd06b4d9..075de8f3f0 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 (opaque,idopt) ->
+        save_lemma_proved_delayed ~proof ~info ~opaque ~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