Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

3 files changed, 10 insertions, 2 deletions

diff --git a/dev/base_include b/dev/base_include
index d1125965..ad2a3aec 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -123,7 +123,6 @@ open Decl_mode
 open Auto
 open Autorewrite
 open Contradiction
-open Dhyp
 open Eauto
 open Elim
 open Equality
@@ -199,6 +198,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
 
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 6a42678e..40a5a822 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -105,12 +105,12 @@ Notation
 Dumpglob
 Reserve
 Impargs
-Constrextern
 Syntax_def
 Implicit_quantifiers
 Smartlocate
 Constrintern
 Modintern
+Constrextern
 Tacexpr
 Proof_type
 Goal
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 3fc90761..3116cbf2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -487,5 +487,9 @@ let short_string_of_ref loc = function
         [id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)]
         (id_of_string ("_"^string_of_int j))
 
+(* Anticipate that printers can be used from ocamldebug and that 
+   pretty-printer should not make calls to the global env since ocamldebug
+   runs in a different process and does not have the proper env at hand *)
+let _ = Constrextern.in_debugger := true
 let _ = Constrextern.set_debug_global_reference_printer
   (if !rawdebug then raw_string_of_ref else short_string_of_ref)