From 420f78b2caeaaddc6fe484565b2d0e49c66888e5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 27 Jul 2014 10:02:38 +0200
Subject: Imported Upstream version 8.4pl4dfsg

---
 tactics/auto.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'tactics/auto.ml')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 44fea151..3451957e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -894,7 +894,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