From 34ae79e9d9ee62e306c035e274428b16564b03b3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Sat, 27 Dec 2014 11:29:44 +0100
Subject: Revert "Term: include a function to print terms"

Such printer is already in Termops

This reverts commit 5d6106a075b79abbb92b03bbca7b13a517cf4925.
---
 kernel/term.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 508d9b81a..3adfa5e37 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -679,10 +679,3 @@ 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