From 66b0c04d4799c023504fe847a4b7b341dcbe92ac Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 7 Oct 2008 13:27:55 +0000
Subject: fixing r11433 again: - backtrack on kernel modifications: the
 monomorphic instance of an inductive   type is constrained to live in an
 universe higher (or equal) than all the   instances - improved support for
 polymorphic inductive types at the refiner level:   introduced
 type_of_inductive_knowing_conclusion that computes the   instance to match
 the current conclusion universe.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11435 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 93d0d96b20..918a32c956 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -147,17 +147,15 @@ let rec make_subst env = function
       let args = match args with _::args -> args | [] -> [] in
       let ctx,subst = make_subst env (sign, exp, args) in
       d::ctx, subst
-  | (na,None,t as d)::sign, Some u::exp, a::args ->
+  | d::sign, Some u::exp, a::args ->
       (* We recover the level of the argument, but we don't change the *)
       (* level in the corresponding type in the arity; this level in the *)
       (* arity is a global level which, at typing time, will be enforce *)
       (* to be greater than the level of the argument; this is probably *)
       (* a useless extra constraint *)
-      let _,ars = dest_arity env a in
-      let s = sort_as_univ ars in
+      let s = sort_as_univ (snd (dest_arity env a)) in
       let ctx,subst = make_subst env (sign, exp, args) in
-      let t = actualize_decl_level env ars t in
-      (na,None,t)::ctx, cons_subst u s subst
+      d::ctx, cons_subst u s subst
   | (na,None,t as d)::sign, Some u::exp, [] ->
       (* No more argument here: we instantiate the type with a fresh level *)
       (* which is first propagated to the corresponding premise in the arity *)
-- 
cgit v1.2.3