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.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 3adfa5e37..508d9b81a 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -679,3 +679,10 @@ let kind_of_type t = match kind_of_term t with | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) -> AtomicType (t,[||]) | (Lambda _ | Construct _) -> failwith "Not a type" + +(* This is not dead code, it is there to have a constr printer available + * everywhere *) +let print_val, print_hook = + Hook.make ~default:(fun x -> Pp.str"constr printer not installed") () +let print t = Hook.get print_val t + -- cgit v1.2.3