aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/univ.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7c9a5ca322..1e7d2c83cb 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -223,7 +223,7 @@ module HList = struct
let rec mem e l =
match l.Hcons.node with
| Nil -> false
- | Cons (x, ll) -> x == e || mem e ll
+ | Cons (x, ll) -> H.equal x e || mem e ll
let rec compare cmp l1 l2 =
if l1 == l2 then 0