diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:16:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:16:31 +0200 |
| commit | cb41d7b40c401c15e9cb66f508f89dbd1bdcdbff (patch) | |
| tree | f852248c2ce2be0cc3e6aae136e961561e395e85 /plugins/funind/indfun_common.ml | |
| parent | e70bec8fba8b15155aca41812225fcf42e1408e0 (diff) | |
| parent | f610068823b33bdc0af752a646df05b98489d7ce (diff) | |
Merge PR#763: [proof] Deprecate redundant wrappers.
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7558ac7ac..6fe6888f3 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -161,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook = let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in - if with_clean then Pfedit.delete_current_proof (); + if with_clean then Proof_global.discard_current (); CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id @@ -173,7 +173,7 @@ let cook_proof _ = let get_proof_clean do_reduce = let result = cook_proof do_reduce in - Pfedit.delete_current_proof (); + Proof_global.discard_current (); result let with_full_print f a = |