[vernac] Allow path for `save_proof` where no proof state is present.

In that case the terminator and proof object have to be supplied in
the ?proof argument, or else we get an anomaly.

Co-authored-by: Maxime Dénès <mail@maximedenes.fr>

3 files changed, 80 insertions, 62 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 19b0856015..1c7cc5e636 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -448,60 +448,65 @@ let () =
       optread  = (fun () -> !keep_admitted_vars);
       optwrite = (fun b -> keep_admitted_vars := b) }
 
-let save_proof ?proof ~pstate = function
-  | Vernacexpr.Admitted ->
-      let pe =
-        let open Proof_global in
-        match proof with
-        | Some ({ id; entries; persistence = k; universes }, _) ->
-            if List.length entries <> 1 then
-              user_err Pp.(str "Admitted does not support multiple statements");
-            let { const_entry_secctx; const_entry_type } = List.hd entries in
-            if const_entry_type = None then
-              user_err Pp.(str "Admitted requires an explicit statement");
-            let typ = Option.get const_entry_type in
-            let ctx = UState.univ_entry ~poly:(pi2 k) universes in
-            let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
-            Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
-        | None ->
-            let pftree = Proof_global.give_me_the_proof pstate in
-            let gk = Proof_global.get_current_persistence pstate 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.((data pftree).initial_euctx) in
-            (* This will warn if the proof is complete *)
-            let pproofs, _univs =
-              Proof_global.return_proof ~allow_partial:true pstate in
-            let sec_vars =
-              if not !keep_admitted_vars then None
-              else match Proof_global.get_used_variables pstate, 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 decl = Proof_global.get_universe_decl pstate in
-            let ctx = UState.check_univ_decl ~poly universes decl in
-            Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
-      in
-    Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe;
-    Some pstate
-  | Vernacexpr.Proved (opaque,idopt) ->
-      let (proof_obj,terminator) =
-        match proof with
-        | None ->
-          Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate
-        | Some proof -> proof
+let save_proof_admitted ?proof ~pstate =
+  let pe =
+    let open Proof_global in
+    match proof with
+    | Some ({ id; entries; persistence = k; universes }, _) ->
+      if List.length entries <> 1 then
+        user_err Pp.(str "Admitted does not support multiple statements");
+      let { const_entry_secctx; const_entry_type } = List.hd entries in
+      if const_entry_type = None then
+        user_err Pp.(str "Admitted requires an explicit statement");
+      let typ = Option.get const_entry_type in
+      let ctx = UState.univ_entry ~poly:(pi2 k) universes in
+      let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
+      Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
+    | None ->
+      let pftree = Proof_global.give_me_the_proof pstate in
+      let gk = Proof_global.get_current_persistence pstate 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
-      (* if the proof is given explicitly, nothing has to be deleted *)
-      let pstate = if Option.is_empty proof then Proof_global.discard_current pstate else Some pstate in
-      Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)));
-      pstate
+      let typ = EConstr.Unsafe.to_constr typ in
+      let universes = Proof.((data pftree).initial_euctx) in
+      (* This will warn if the proof is complete *)
+      let pproofs, _univs =
+        Proof_global.return_proof ~allow_partial:true pstate in
+      let sec_vars =
+        if not !keep_admitted_vars then None
+        else match Proof_global.get_used_variables pstate, 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 decl = Proof_global.get_universe_decl pstate in
+      let ctx = UState.check_univ_decl ~poly universes decl in
+      Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
+  in
+  Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe
+
+let save_proof_proved ?proof ?pstate ~opaque ~idopt =
+  (* Invariant (uh) *)
+  if Option.is_empty pstate && Option.is_empty proof then
+    user_err (str "No focused proof (No proof-editing in progress).");
+  let (proof_obj,terminator) =
+    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 pstate = Option.get pstate in
+      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate
+    | Some proof -> proof
+  in
+  (* if the proof is given explicitly, nothing has to be deleted *)
+  let pstate = if Option.is_empty proof then Proof_global.discard_current Option.(get pstate) else pstate in
+  Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)));
+  pstate
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 9b5c84e0d1..1f70cfa1ad 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -71,4 +71,14 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** {6 ... } *)
 
-val save_proof : ?proof:Proof_global.closed_proof -> pstate:Proof_global.t -> Vernacexpr.proof_end -> Proof_global.t option
+val save_proof_admitted
+  :  ?proof:Proof_global.closed_proof
+  -> pstate:Proof_global.t
+  -> unit
+
+val save_proof_proved
+  :  ?proof:Proof_global.closed_proof
+  -> ?pstate:Proof_global.t
+  -> opaque:Proof_global.opacity_flag
+  -> idopt:Names.lident option
+  -> Proof_global.t option
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3ead8663ce..284df19b4c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -616,15 +616,18 @@ let vernac_start_proof ~atts ~pstate kind l =
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
   Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
 
-let vernac_end_proof ~pstate ?proof = function
-  | Admitted          -> save_proof ~pstate ?proof Admitted
-  | Proved (_,_) as e -> save_proof ~pstate ?proof e
+let vernac_end_proof ?pstate ?proof = function
+  | Admitted ->
+    vernac_require_open_proof ~pstate (save_proof_admitted ?proof);
+    pstate
+  | Proved (opaque,idopt) ->
+    save_proof_proved ?pstate ?proof ~opaque ~idopt
 
 let vernac_exact_proof ~pstate c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
   let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in
-  let pstate = save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Opaque,None))) in
+  let pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom;
   pstate
 
@@ -2270,7 +2273,7 @@ let interp ?proof ~atts ~st c : Proof_global.t option =
     with_def_attributes ~atts vernac_start_proof ~pstate k l
   | VernacEndProof e ->
     unsupported_attributes atts;
-    vernac_require_open_proof ~pstate (vernac_end_proof ?proof e)
+    vernac_end_proof ?proof ?pstate e
   | VernacExactProof c ->
     unsupported_attributes atts;
     vernac_require_open_proof ~pstate (vernac_exact_proof c)