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
---
 interp/constrextern.ml  | 1 -
 interp/constrextern.mli | 1 +
 2 files changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bd8e78c0f5..b3810bb6d4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -143,7 +143,6 @@ let debug_global_reference_printer =
 let in_debugger = ref false
 
 let set_debug_global_reference_printer f =
-  in_debugger := true;
   debug_global_reference_printer := f
 
 let extern_reference loc vars r =
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index e1fdd068b7..2a53eb85fe 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -53,6 +53,7 @@ val print_projections : bool ref
 (** Debug printing options *)
 val set_debug_global_reference_printer :
   (loc -> global_reference -> reference) -> unit
+val in_debugger : bool ref
 
 (** This governs printing of implicit arguments. If [with_implicits] is
    on and not [with_arguments] then implicit args are printed prefixed
-- 
cgit v1.2.3