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, 0 insertions, 6 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index 972f7d5d8..c5e85b1e5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -480,9 +480,3 @@ 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
-