Merge PR #8999: [pfedit] Remove cook_proof stub.

2 files changed, 16 insertions, 13 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d537436c6b..437eee3413 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -306,17 +306,18 @@ let universe_proof_terminator compute_guard hook =
   | Admitted (id,k,pe,ctx) ->
       admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
       Feedback.feedback Feedback.AddedAxiom
-  | Proved (opaque,idopt,proof) ->
-      let is_opaque, export_seff = match opaque with
-        | Transparent -> false, true
-        | Opaque      -> true, false
-      in
-      let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in
-      let const = {const with const_entry_opaque = is_opaque} in
-      let id = match idopt with
-        | None -> id
-        | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
-      save ~export_seff id const univs compute_guard persistence (hook (Some univs))
+  | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
+    let is_opaque, export_seff = match opaque with
+      | Transparent -> false, true
+      | Opaque      -> true, false
+    in
+    let const = {const with const_entry_opaque = is_opaque} in
+    let id = match idopt with
+      | None -> id
+      | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
+    save ~export_seff id const universes compute_guard persistence (hook (Some universes))
+  | Proved (opaque,idopt, _ ) ->
+    CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
   end
 
 let standard_proof_terminator compute_guard hook =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c2805674e4..746db61cc3 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -844,8 +844,7 @@ let obligation_terminator name num guard hook auto pf =
   let term = Lemmas.universe_proof_terminator guard hook in
   match pf with
   | Admitted _ -> apply_terminator term pf
-  | Proved (opq, id, proof) ->
-    let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
+  | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
     let env = Global.env () in
     let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
     let ty = entry.Entries.const_entry_type in
@@ -904,6 +903,9 @@ let obligation_terminator name num guard hook auto pf =
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
       pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
+  end
+  | Proved (_, _, _ ) ->
+    CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
 
 let obligation_hook prg obl num auto ctx' _ gr =
   let obls, rem = prg.prg_obligations in