From e3e4687715ee2839f4d326cb225ba4a586b8a48a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Nov 2018 03:42:07 +0100
Subject: [pfedit] Remove cook_proof stub.

This is barely used and not very useful, clients should use the
close_proof API directly.
---
 proofs/pfedit.ml  | 23 +++++++++--------------
 proofs/pfedit.mli | 15 ---------------
 2 files changed, 9 insertions(+), 29 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7b55941874..78080fa203 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -35,16 +35,6 @@ let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
     | None -> p,(true,[])
     | Some tac -> Proof.run_tactic env tac p))
 
-let cook_this_proof p =
-  match p with
-  | { Proof_global.id;entries=[constr];persistence;universes } ->
-      (id,(constr,universes,persistence))
-  | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
-
-let cook_proof () =
-  cook_this_proof (fst
-    (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
-
 exception NoSuchGoal
 let _ = CErrors.register_handler begin function
   | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
@@ -155,10 +145,15 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   start_proof id goal_kind evd sign typ terminator;
   try
     let status = by tac in
-    let _,(const,univs,_) = cook_proof () in
-    Proof_global.discard_current ();
-    let univs = UState.demote_seff_univs const univs in
-    const, status, univs
+    let open Proof_global in
+    let { entries; universes } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+    match entries with
+    | [entry] ->
+      discard_current ();
+      let univs = UState.demote_seff_univs entry universes in
+      entry, status, univs
+    | _ ->
+      CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
   with reraise ->
     let reraise = CErrors.push reraise in
     Proof_global.discard_current ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 50ce267c81..76be7936b4 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -28,21 +28,6 @@ val start_proof :
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
-(** {6 ... } *)
-(** [cook_proof opacity] turns the current proof (assumed completed) into
-    a constant with its name, kind and possible hook (see [start_proof]);
-    it fails if there is no current proof of if it is not completed;
-    it also tells if the guardness condition has to be inferred. *)
-
-val cook_this_proof :
-    Proof_global.proof_object ->
-  (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
-
-val cook_proof : unit ->
-  (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
-
 (** {6 ... } *)
 (** [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
-- 
cgit v1.2.3