From 41b3d9d0432ae3522ed14e69b38dcf405a31df8c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 Jun 2014 13:06:14 +0200
Subject: Fix type_of_inductive_knowing_conclusion, relying on an actually
 broken univ_depends. Also add a missing constraint when generating a fresh
 universe for a template polymorphic inductive in that case.

---
 kernel/univ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

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 
-- 
cgit v1.2.3