aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.mli')
-rw-r--r--kernel/term.mli6
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index c5e85b1e5..972f7d5d8 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -480,3 +480,9 @@ val hcons_constr : constr -> constr
val hcons_types : types -> types
(** Alias for [Constr.hashcons] *)
+
+
+(********************** debugging ************************************)
+val print_hook : (constr -> Pp.std_ppcmds) Hook.t
+val print : constr -> Pp.std_ppcmds
+