diff options
| author | Emilio Jesus Gallego Arias | 2018-04-08 03:51:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:22:50 +0100 |
| commit | 54a2a3a07e14c597b264566e01d2ecc69c4bd90c (patch) | |
| tree | 52defd39c09a3f981859e053e80946b5495c2039 /tactics/hints.ml | |
| parent | 3b95c063fae710bc7a943e0dd02617bac09c21bc (diff) | |
[tactic] Adapt tactic layer to removal of imperative proof state.
State in `Proof_global` was mostly used for debugging, so not a big
change.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 85d75f1010..3a7e67cb3f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1514,9 +1514,9 @@ let pr_hint_term env sigma cl = (str "No hint applicable for current goal") (* print all hints that apply to the concl of the current goal *) -let pr_applicable_hint () = +let pr_applicable_hint pf = let env = Global.env () in - let pts = Proof_global.give_me_the_proof () in + let pts = Proof_global.give_me_the_proof pf in let Proof.{goals;sigma} = Proof.data pts in match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") |