summaryrefslogtreecommitdiff
path: root/interp/constrextern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.mli')
-rw-r--r--interp/constrextern.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index e1fdd068..2a53eb85 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