diff options
| author | Maxime Dénès | 2017-06-14 18:16:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 18:16:31 +0200 |
| commit | cb41d7b40c401c15e9cb66f508f89dbd1bdcdbff (patch) | |
| tree | f852248c2ce2be0cc3e6aae136e961561e395e85 /tactics/hints.ml | |
| parent | e70bec8fba8b15155aca41812225fcf42e1408e0 (diff) | |
| parent | f610068823b33bdc0af752a646df05b98489d7ce (diff) | |
Merge PR#763: [proof] Deprecate redundant wrappers.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 3 |
1 files changed, 1 insertions, 2 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.") |