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

7 files changed, 34 insertions, 65 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d1e7d8a5a8..1cf952576d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -320,10 +320,16 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
     (* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
     (* 	end; *)
-    get_proof_clean true, CEphemeron.create hook
-  end
-
 
+      let open Proof_global in
+      let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+      match entries with
+      | [entry] ->
+        discard_current ();
+        (id,(entry,persistence)), CEphemeron.create hook
+      | _ ->
+        CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
+  end
 
 let generate_functional_principle (evd: Evd.evar_map ref)
     interactive_proof
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index cd2ea3ef88..b68b34ca35 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -147,17 +147,6 @@ let save with_clean id const (locality,_,kind) hook =
   CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
   definition_message id
 
-
-
-let cook_proof _ =
-  let (id,(entry,_,strength)) = Pfedit.cook_proof () in
-  (id,(entry,strength))
-
-let get_proof_clean do_reduce =
-  let result = cook_proof do_reduce in
-  Proof_global.discard_current ();
-  result
-
 let with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0c8f40c5cf..c9d153d89f 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -45,15 +45,6 @@ val jmeq_refl : unit -> EConstr.constr
 val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
   Lemmas.declaration_hook CEphemeron.key -> unit
 
-(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
-   abort the proof
-*)
-val get_proof_clean : bool ->
-  Names.Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind)
-
-
-
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
 
    This function preserves the print settings
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 *)
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