From 3be4b91c09e6ec816aada997fc245484abfa1f05 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 1 Feb 2012 08:57:50 +0000
Subject: Debugger vs tracer: Two different behaviors wrt printing: The
 debugger runs in separate process. It has no access to the global env and it
 should not request it. The tracer runs in the same process as Coq and has
 full access to the global env and to regular pretty-printing of global names.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14958 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index d112596502..1c794a3ae9 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -199,6 +199,11 @@ let current_goal () = get_nth_goal 1;;
 let pf_e gl s = 
   Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);;
 
+(* Set usual printing since the global env is available from the tracer *)
+let _ = Constrextern.in_debugger := false
+let _ = Constrextern.set_debug_global_reference_printer
+  (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+
 open Toplevel
 let go = loop
 
-- 
cgit v1.2.3