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. --- interp/constrextern.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'interp/constrextern.mli') diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 023c5be22..804795480 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -59,8 +59,6 @@ val set_extern_reference : val get_extern_reference : unit -> (Loc.t -> Id.Set.t -> global_reference -> reference) -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 by "!"; if [with_implicits] and [with_arguments] are both on the -- cgit v1.2.3