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.
---
 plugins/funind/indfun_common.ml | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'plugins/funind/indfun_common.ml')

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 ()
-- 
cgit v1.2.3