diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-24 14:34:51 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-26 15:07:03 +0100 |
commit | 5d6106a075b79abbb92b03bbca7b13a517cf4925 (patch) | |
tree | 8dd90fb5483a623b27f3d62a18e7a6cf088fc4af /kernel/term.mli | |
parent | dca4b978ff8bfa2eeee864edac4199d9d9df3d5e (diff) |
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.
Diffstat (limited to 'kernel/term.mli')
-rw-r--r-- | kernel/term.mli | 6 |
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 + |