From 34ae79e9d9ee62e306c035e274428b16564b03b3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
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 -------
 kernel/term.mli | 6 ------
 2 files changed, 13 deletions(-)

(limited to 'kernel')

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