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

3 files changed, 9 insertions, 23 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