aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.mli')
-rw-r--r--kernel/constr.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 98bf71308..19ffa8fe3 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -459,7 +459,3 @@ val case_info_hash : case_info -> int
(*********************************************************************)
val hcons : constr -> constr
-
-(**************************************)
-
-type values