aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.mli')
-rw-r--r--kernel/term.mli6
1 files changed, 0 insertions, 6 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index b0387417c..b5304b651 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -543,9 +543,3 @@ val hcons1_types : types -> types
(**************************************)
type values
-
-
-(*************************************************************)
-
-(* spiwack: printing of internal representation of constr *)
-val string_of_constr : constr -> string