From 6119a0e4f760ff944351570e90487f066db42858 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Sep 2014 18:42:21 +0200
Subject: Fixing printing of unreachable local tactics.

---
 printing/pptactic.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 87fb500ef0..890e0d585b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -343,7 +343,10 @@ let pr_ltac_or_var pr = function
 
 let pr_ltac_constant kn =
   if !Constrextern.in_debugger then pr_kn kn
-  else pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+  else try
+    pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+  with Not_found -> (* local tactic not accessible anymore *)
+    str "<" ++ pr_kn kn ++ str ">"
 
 let pr_evaluable_reference_env env = function
   | EvalVarRef id -> pr_id id
-- 
cgit v1.2.3