From 23041481ff368b0b4cfc9a2493c9f465df90ea90 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 18 Sep 2014 21:39:03 +0200 Subject: Fix debug printing with primitive projections. Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit. --- dev/base_include | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dev/base_include') diff --git a/dev/base_include b/dev/base_include index 2699551a5..1d43e64df 100644 --- a/dev/base_include +++ b/dev/base_include @@ -210,7 +210,8 @@ let pf_e gl s = Constrintern.interp_constr (pf_env gl) (project gl) (parse_constr s);; (* Set usual printing since the global env is available from the tracer *) -let _ = Constrextern.in_debugger := false +let _ = Flags.in_debugger := false +let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; -- cgit v1.2.3