aboutsummaryrefslogtreecommitdiff
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, 6 insertions, 0 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index 0d40da9691..4133ca8920 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -547,3 +547,9 @@ val hcons1_types : types -> types
(**************************************)
type values
+
+
+(*************************************************************)
+
+(* spiwack: printing of internal representation of constr *)
+val string_of_constr : constr -> string