From 1c6c4d1a4b7bc4c4a4a14df44c44a860bb0ce81e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Jan 2014 19:17:03 +0100
Subject: Fixing bug #1758: Print Hint output can be misleading if variable
 shadows hypothesis.

---
 tactics/auto.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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 ())
-- 
cgit v1.2.3