aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.mli')
-rw-r--r--kernel/constr.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 261b6bfb4..858af97b6 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -236,6 +236,7 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
(** {6 Hashconsing} *)
val hash : constr -> int
+val case_info_hash : case_info -> int
(*********************************************************************)