diff options
| author | Pierre-Marie Pédrot | 2014-01-16 19:17:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-17 12:19:20 +0100 |
| commit | 1c6c4d1a4b7bc4c4a4a14df44c44a860bb0ce81e (patch) | |
| tree | 9354188216727ac217cd1b69260d898195363455 | |
| parent | 8af364e7702d6949a92399d5e6965a83e06b9866 (diff) | |
Fixing bug #1758: Print Hint output can be misleading if variable shadows hypothesis.
| -rw-r--r-- | tactics/auto.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index fc9a335e68..74a1c56244 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -908,7 +908,13 @@ let pr_autotactic = (str"apply " ++ pr_constr c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> - (str "(*external*) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) + let env = + try + let (_, env) = Pfedit.get_current_goal_context () in + env + with e when Errors.noncritical e -> Global.env () + in + (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac) let pr_hint (id, v) = (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) |