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 +-
 pretyping/inductiveops.ml | 6 ++++--
 2 files changed, 5 insertions(+), 3 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 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 21395af027..c64cd35e53 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -480,14 +480,16 @@ let rec instantiate_universes env evdref scl is = function
       d :: instantiate_universes env evdref scl is (sign, exp)
   | (na,None,ty)::sign, Some u::exp ->
       let ctx,_ = Reduction.dest_arity env ty in
+      let u = Univ.Universe.make u in
       let s =
 	(* Does the sort of parameter [u] appear in (or equal)
            the sort of inductive [is] ? *)
-        if univ_depends (Univ.Universe.make u) is then
+        if univ_depends u is then
           scl (* constrained sort: replace by scl *)
         else
-          (* unconstriained sort: replace by fresh universe *)
+          (* unconstrained sort: replace by fresh universe *)
           let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in
+	  let evm = Evd.set_leq_sort evm s (Sorts.sort_of_univ u) in
 	    evdref := evm; s
       in
       (na,None,mkArity(ctx,s)):: instantiate_universes env evdref scl is (sign, exp)
-- 
cgit v1.2.3