diff options
| author | Pierre-Marie Pédrot | 2018-11-19 13:36:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:36:24 +0100 |
| commit | d73fee2674999225ce59cc0a9f61dfafe99d7689 (patch) | |
| tree | 2501d86e9ff5166d31662de6b4fd1b0bc1679033 /plugins/funind/indfun_common.ml | |
| parent | df2757b19b2be69aa2e026343221dbe185e3a0df (diff) | |
| parent | e3e4687715ee2839f4d326cb225ba4a586b8a48a (diff) | |
Merge PR #8999: [pfedit] Remove cook_proof stub.
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 11 |
1 files changed, 0 insertions, 11 deletions
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 () |