From 5d6106a075b79abbb92b03bbca7b13a517cf4925 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 24 Dec 2014 14:34:51 +0100
Subject: Term: include a function to print terms

I find it very odd not to have a pretty printer for terms than can
be called from *everywhere*.  This commit sticks in Term a long spaghetti
to let Printer install a printing function.
---
 kernel/term.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index c5e85b1e5e..972f7d5d89 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
+
-- 
cgit v1.2.3