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

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

6 files changed, 139 insertions, 145 deletions

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