From 65e645a5f533b7af5b75fc68e4e9486884f4f600 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Jan 2013 14:36:01 +0000
Subject: Avoid failure in debugger when printing Ltac names.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16152 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/pptactic.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 5b33f89cb3..5a53968755 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -317,8 +317,9 @@ let pr_ltac_or_var pr = function
   | ArgArg x -> pr x
   | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
 
-let pr_ltac_constant sp =
-  pr_qualid (Nametab.shortest_qualid_of_tactic sp)
+let pr_ltac_constant kn =
+  if !Constrextern.in_debugger then pr_kn kn
+  else pr_qualid (Nametab.shortest_qualid_of_tactic kn)
 
 let pr_evaluable_reference_env env = function
   | EvalVarRef id -> pr_id id
-- 
cgit v1.2.3