aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cSig.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/cSig.mli')
-rw-r--r--lib/cSig.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 4463e8d9c..796e58cbf 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -14,6 +14,8 @@ type ('a, 'b) union = Inl of 'a | Inr of 'b
type 'a until = Stop of 'a | Cont of 'a
(** Used for browsable-until structures. *)
+type (_, _) eq = Refl : ('a, 'a) eq
+
module type SetS =
sig
type elt