summaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /dev
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include6
-rw-r--r--dev/printers.mllib2
-rw-r--r--dev/top_printers.ml4
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)