diff options
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r-- | tactics/auto.ml | 10 |
1 files changed, 8 insertions, 2 deletions
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 ()) |