diff options
| author | Emilio Jesus Gallego Arias | 2017-06-11 06:08:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-11 15:54:48 +0200 |
| commit | f610068823b33bdc0af752a646df05b98489d7ce (patch) | |
| tree | 5d664bd1b3efb43536250b30b0dffa724e28dba4 /plugins/funind | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
[proof] Deprecate redundant wrappers.
As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.
We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index fd4b52b65c..de5a5685b5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -371,12 +371,12 @@ let generate_functional_principle (evd: Evd.evar_map ref) begin begin try - let id = Pfedit.get_current_proof_name () in + let id = Proof_global.get_current_proof_name () in let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () + then Proof_global.discard_current () else () else () with e when CErrors.noncritical e -> () @@ -524,12 +524,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con begin begin try - let id = Pfedit.get_current_proof_name () in + let id = Proof_global.get_current_proof_name () in let s = Id.to_string id in let n = String.length "___________princ_________" in if String.length s >= n then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () + then Proof_global.discard_current () else () else () with e when CErrors.noncritical e -> () diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8f62231aeb..b824c3e293 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 = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index bd74d2cf64..b1c69812dc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1295,7 +1295,7 @@ let is_opaque_constant c = let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = get_current_proof_name () in + let current_proof_name = Proof_global.get_current_proof_name () in let name = match goal_name with | Some s -> s | None -> |