fixed pb with r11433

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11434 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 2 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 10e6569ca..93d0d96b2 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -153,9 +153,10 @@ let rec make_subst env = function
       (* 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 s = sort_as_univ (snd (dest_arity env a)) in
+      let _,ars = dest_arity env a in
+      let s = sort_as_univ ars in
       let ctx,subst = make_subst env (sign, exp, args) in
-      let t = actualize_decl_level env (Type s) t in
+      let t = actualize_decl_level env ars t in
       (na,None,t)::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 *)