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.

---
 pretyping/inductiveops.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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