[pfedit] Remove cook_proof stub.

This is barely used and not very useful, clients should use the
close_proof API directly.

2 files changed, 9 insertions, 29 deletions

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
@@ -29,21 +29,6 @@ val start_proof :
   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
    focused proof or if there is no more subgoals *)