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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/hints.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 11 |
2 files changed, 6 insertions, 8 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 773abb9f0c..681db5d08e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -29,7 +29,6 @@ open Decl_kinds open Pattern open Patternops open Clenv -open Pfedit open Tacred open Printer open Vernacexpr @@ -1462,7 +1461,7 @@ let pr_hint_term sigma cl = (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint () = - let pts = get_pftreestate () in + let pts = Proof_global.give_me_the_proof () in let glss = Proof.V82.subgoals pts in match glss.Evd.it with | [] -> CErrors.user_err Pp.(str "No focused goal.") diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b553f316c2..7e560b1762 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -25,7 +25,6 @@ open Inductiveops open Reductionops open Globnames open Evd -open Pfedit open Tacred open Genredexpr open Tacmach.New @@ -543,7 +542,7 @@ end let fix ido n = match ido with | None -> Proofview.Goal.enter begin fun gl -> - let name = Pfedit.get_current_proof_name () in + let name = Proof_global.get_current_proof_name () in let id = new_fresh_id [] name gl in mutual_fix id n [] 0 end @@ -594,7 +593,7 @@ end let cofix ido = match ido with | None -> Proofview.Goal.enter begin fun gl -> - let name = Pfedit.get_current_proof_name () in + let name = Proof_global.get_current_proof_name () in let id = new_fresh_id [] name gl in mutual_cofix id [] 0 end @@ -1140,7 +1139,7 @@ let rec intros_move = function let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = solve_by_implicit_tactic (); + Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } @@ -5032,11 +5031,11 @@ let name_op_to_name name_op object_kind suffix = let default_gk = (Global, false, object_kind) in match name_op with | Some s -> - (try let _, gk, _ = current_proof_statement () in s, gk + (try let _, gk, _ = Pfedit.current_proof_statement () in s, gk with NoCurrentProof -> s, default_gk) | None -> let name, gk = - try let name, gk, _ = current_proof_statement () in name, gk + try let name, gk, _ = Pfedit.current_proof_statement () in name, gk with NoCurrentProof -> anon_id, default_gk in add_suffix name suffix, gk |