Nouvelle implantation du polymorphisme de sorte pour les familles inductives

- prise en compte du niveau à la déclaration du type comme une fonction
  des sortes des conclusions des paramètres uniformes
- suppression du retypage de chaque instance de type inductif (trop coûteux)
  et donc abandon de l'idée de calculer une sorte minimale même dans
  des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t.


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

17 files changed, 394 insertions, 309 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8eb29c4dd..17a8d5ac9 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -45,6 +45,13 @@ type constant_body = {
 (*s Inductive types (internal representation with redundant
     information). *)
 
+let subst_rel_declaration sub (id,copt,t as x) =
+  let copt' = option_smartmap (subst_mps sub) copt in
+  let t' = subst_mps sub t in
+  if copt == copt' & t == t' then x else (id,copt',t')
+
+let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
+
 type recarg = 
   | Norec 
   | Mrec of int 
@@ -83,6 +90,20 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
    with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
 *)
 
+type polymorphic_inductive_arity = {
+  mind_param_levels : universe option list;
+  mind_level : universe;
+}
+
+type monomorphic_inductive_arity = {
+  mind_user_arity : constr;
+  mind_sort : sorts;
+}
+
+type inductive_arity = 
+| Monomorphic of monomorphic_inductive_arity
+| Polymorphic of polymorphic_inductive_arity
+
 type one_inductive_body = {
 
 (* Primitive datas *)
@@ -90,8 +111,11 @@ type one_inductive_body = {
  (* Name of the type: [Ii] *)
     mind_typename : identifier;
 
- (* Arity of [Ii] with parameters: [forall params, Ui] *)
-    mind_user_arity : types;
+ (* Arity context of [Ii] with parameters: [forall params, Ui] *)
+    mind_arity_ctxt : rel_context;
+
+ (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *)
+    mind_arity : inductive_arity;
 
  (* Names of the constructors: [cij] *)
     mind_consnames : identifier array;
@@ -103,15 +127,9 @@ type one_inductive_body = {
 
 (* Derived datas *)
 
- (* Head normalized arity so that the conclusion is a sort *)
-    mind_nf_arity : types;
-
  (* Number of expected real arguments of the type (no let, no params) *)
     mind_nrealargs : int;
 
- (* Conclusion of the arity *)
-    mind_sort : sorts;
-
  (* List of allowed elimination sorts *)
     mind_kelim : sorts_family list;
 
@@ -172,23 +190,28 @@ type mutual_inductive_body = {
 let subst_const_body sub cb = {
     const_hyps = (assert (cb.const_hyps=[]); []);
     const_body = option_map (subst_constr_subst sub) cb.const_body;
-    const_type = type_app (subst_mps sub) cb.const_type;
+    const_type = subst_mps sub cb.const_type;
     const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
     (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
     const_constraints = cb.const_constraints;
     const_opaque = cb.const_opaque } 
 
+let subst_arity sub = function
+| Monomorphic s ->
+    Monomorphic {
+      mind_user_arity = subst_mps sub s.mind_user_arity;
+      mind_sort = s.mind_sort;
+    }
+| Polymorphic s as x -> x
+
 let subst_mind_packet sub mbp = 
   { mind_consnames = mbp.mind_consnames;
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = 
-      array_smartmap (type_app (subst_mps sub)) mbp.mind_nf_lc;
-    mind_nf_arity = type_app (subst_mps sub) mbp.mind_nf_arity;
-    mind_user_lc = 
-      array_smartmap (type_app (subst_mps sub)) mbp.mind_user_lc;
-    mind_user_arity = type_app (subst_mps sub) mbp.mind_user_arity;
-    mind_sort = mbp.mind_sort;
+    mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc;
+    mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
+    mind_arity = subst_arity sub mbp.mind_arity;
+    mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_kelim = mbp.mind_kelim;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index bd689ced3..2cbdc3eb3 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -70,6 +70,20 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 \end{verbatim}
 *)
 
+type polymorphic_inductive_arity = {
+  mind_param_levels : universe option list;
+  mind_level : universe;
+}
+
+type monomorphic_inductive_arity = {
+  mind_user_arity : constr;
+  mind_sort : sorts;
+}
+
+type inductive_arity = 
+| Monomorphic of monomorphic_inductive_arity
+| Polymorphic of polymorphic_inductive_arity
+
 type one_inductive_body = {
 
 (* Primitive datas *)
@@ -77,8 +91,11 @@ type one_inductive_body = {
  (* Name of the type: [Ii] *)
     mind_typename : identifier;
 
- (* Arity of [Ii] with parameters: [forall params, Ui] *)
-    mind_user_arity : types;
+ (* Arity context of [Ii] with parameters: [forall params, Ui] *)
+    mind_arity_ctxt : rel_context;
+
+ (* Arity sort and original user arity if monomorphic *)
+    mind_arity : inductive_arity;
 
  (* Names of the constructors: [cij] *)
     mind_consnames : identifier array;
@@ -90,15 +107,9 @@ type one_inductive_body = {
 
 (* Derived datas *)
 
- (* Head normalized arity so that the conclusion is a sort *)
-    mind_nf_arity : types;
-
  (* Number of expected real arguments of the type (no let, no params) *)
     mind_nrealargs : int;
 
- (* Conclusion of the arity *)
-    mind_sort : sorts;
-
  (* List of allowed elimination sorts *)
     mind_kelim : sorts_family list;
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d47a796ef..b5de04221 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -119,7 +119,7 @@ let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
 
 (* An inductive definition is a "unit" if it has only one constructor
    and that all arguments expected by this constructor are 
-   logical, this is the case for equality, conjonction of logical properties 
+   logical, this is the case for equality, conjunction of logical properties 
 *)
 let is_unit constrsinfos =
   match constrsinfos with  (* One info = One constructor *)
@@ -143,45 +143,54 @@ let small_unit constrsinfos =
   and isunit = is_unit constrsinfos in
   issmall, isunit
 
-(* This (re)computes informations relevant to extraction and the sort of an
-   arity or type constructor; we do not to recompute universes constraints *)
+(* Computing the levels of polymorphic inductive types
+
+   For each inductive type of a block that is of level u_i, we have
+   the constraints that u_i >= v_i where v_i is the type level of the
+   types of the constructors of this inductive type. Each v_i depends
+   of some of the u_i and of an extra (maybe non variable) universe,
+   say w_i that summarize all the other constraints. Typically, for
+   three inductive types, we could have
 
-(* [smax] is the max of the sorts of the products of the constructor type *)
+   u1,u2,u3,w1 <= u1
+   u1       w2 <= u2
+      u2,u3,w3 <= u3
 
-let enforce_type_constructor env arsort smax cst =
-  match smax, arsort with
-    | Type uc, Type ua -> enforce_geq ua uc cst
-    | Type uc, Prop Pos when engagement env <> Some ImpredicativeSet ->
-        error "Large non-propositional inductive types must be in Type"
-    | _,_ -> cst
+   From this system of inequations, we shall deduce
 
-let type_one_constructor env_ar_par params arsort c =
-  let infos = infos_and_sort env_ar_par c in
+   w1,w2,w3 <= u1
+   w1,w2 <= u2
+   w1,w2,w3 <= u3
+*)   
 
-  (* Each constructor is typed-checked here *)
-  let (j,cst) = infer_type env_ar_par c in
-  let full_cstr_type = it_mkProd_or_LetIn j.utj_val params in
+let inductive_levels arities inds =
+  let levels = Array.map (function _,_,Type u -> Some u | _ -> None) arities in
+  let cstrs_levels = Array.map (fun (_,_,_,_,_,lev) -> lev) inds in
+  (* Take the transitive closure of the system of constructors *)
+  (* level constraints and remove the recursive dependencies *)
+  solve_constraints_system levels cstrs_levels
 
-  (* If the arity is at some level Type arsort, then the sort of the
-     constructor must be below arsort; here we consider constructors with the
-     global parameters (which add a priori more constraints on their sort) *)
-  let cst2 = enforce_type_constructor env_ar_par arsort j.utj_type cst in
+(* This (re)computes informations relevant to extraction and the sort of an
+   arity or type constructor; we do not to recompute universes constraints *)
 
-  (infos, full_cstr_type, cst2)
+let constraint_list_union =
+  List.fold_left Constraint.union Constraint.empty
 
-let infer_constructor_packet env_ar params arsort lc =
+let infer_constructor_packet env_ar params lc =
+  (* builds the typing context "Gamma, I1:A1, ... In:An, params" *)
   let env_ar_par = push_rel_context params env_ar in
-  let (constrsinfos,jlc,cst) = 
-    List.fold_right
-      (fun c (infosl,l,cst) ->
-	 let (infos,ct,cst') = 
-	   type_one_constructor env_ar_par params arsort c in
-	 (infos::infosl,ct::l, Constraint.union cst cst'))
-      lc
-      ([],[],Constraint.empty) in
-  let lc' = Array.of_list jlc in
-  let issmall,isunit = small_unit constrsinfos in
-  (issmall,isunit,lc',cst)
+  (* type-check the constructors *)
+  let jlc,cstl = List.split (List.map (infer_type env_ar_par) lc) in
+  let cst = constraint_list_union cstl in
+  let jlc = Array.of_list jlc in
+  (* generalize the constructor over the parameters *)
+  let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in
+  (* compute the max of the sorts of the products of the constructor type *)
+  let level = max_inductive_sort (Array.map (fun j -> j.utj_type) jlc) in
+  (* compute *)
+  let info = small_unit (List.map (infos_and_sort env_ar_par) lc) in
+
+  (info,lc'',level,cst)
 
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
@@ -190,50 +199,75 @@ let typecheck_inductive env mie =
   (* Check unicity of names *)
   mind_check_names mie;
   mind_check_arities env mie;
-         (* Params are typed-checked here *)
-  let params = mie.mind_entry_params in
-  let env_params, params, cstp = infer_local_decls env params in
+  (* Params are typed-checked here *)
+  let env_params, params, cst1 = infer_local_decls env mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows to build the environment of arities and to share *)
   (* the set of constraints *)
-  let cst, arities, rev_params_arity_list =
+  let cst, env_arities, rev_arity_list =
     List.fold_left
-      (fun (cst,arities,l) ind ->
+      (fun (cst,env_ar,l) ind ->
          (* Arities (without params) are typed-checked here *)
-	 let arity, cst2 =
-           infer_type env_params ind.mind_entry_arity in
+	 let arity, cst2 = infer_type env_params ind.mind_entry_arity in
 	 (* We do not need to generate the universe of full_arity; if
 	    later, after the validation of the inductive definition,
 	    full_arity is used as argument or subject to cast, an
 	    upper universe will be generated *)
-	 let id = ind.mind_entry_typename in
 	 let full_arity = it_mkProd_or_LetIn arity.utj_val params in
-	 Constraint.union cst cst2,
-	 Sign.add_rel_decl (Name id, None, full_arity) arities,
-         (params, id, full_arity, arity.utj_val)::l)
-      (cstp,empty_rel_context,[])
+	 let cst = Constraint.union cst cst2 in
+	 let id = ind.mind_entry_typename in
+	 let env_ar' = push_rel (Name id, None, full_arity) env_ar in
+	 let lev = snd (dest_arity env_params arity.utj_val) in
+         (cst,env_ar',(id,full_arity,lev)::l))
+      (cst1,env,[])
       mie.mind_entry_inds in
 
-  let env_arities = push_rel_context arities env in
-
-  let params_arity_list = List.rev rev_params_arity_list in
+  let arity_list = List.rev rev_arity_list in
 
   (* Now, we type the constructors (without params) *)
   let inds,cst =
     List.fold_right2
-      (fun ind (params,id,full_arity,short_arity) (inds,cst) ->
-	 let (_,arsort) = dest_arity env full_arity in
-	 let lc = ind.mind_entry_lc in
-	 let (issmall,isunit,lc',cst') =
-	   infer_constructor_packet env_arities params arsort lc in
+      (fun ind (id,full_arity,_) (inds,cst) ->
+	 let (info,lc',cstrs_univ,cst') =
+	   infer_constructor_packet env_arities params ind.mind_entry_lc in
 	 let consnames = ind.mind_entry_consnames in
-	 let ind' = (id,full_arity,consnames,issmall,isunit,lc')
-	 in
+	 let ind' = (id,full_arity,consnames,info,lc',cstrs_univ) in
 	 (ind'::inds, Constraint.union cst cst'))
       mie.mind_entry_inds
-      params_arity_list
+      arity_list
       ([],cst) in
-  (env_arities, params, Array.of_list inds, cst)
+
+  let inds = Array.of_list inds in
+  let arities = Array.of_list arity_list in
+  let param_ccls = List.fold_left (fun l (_,b,p) ->
+    if b = None then 
+      let _,c = dest_prod_assum env p in
+      let u = match kind_of_term c with Sort (Type u) -> Some u | _ -> None in
+      u::l
+    else 
+      l) [] params in
+
+  (* Compute/check the sorts of the inductive types *)
+  let ind_min_levels = inductive_levels arities inds in
+  let inds =
+    array_map2 (fun (id,full_arity,cn,info,lc,_) lev ->
+      let sign, s = dest_arity env full_arity in
+      let status = match s with
+      | Type _ ->
+	  (* The polymorphic level is a function of the level of the *)
+	  (* conclusions of the parameters *)
+	  Inr (param_ccls, lev)
+      | Prop Pos when engagement env <> Some ImpredicativeSet ->
+	  (* Predicative set: check that the content is indeed predicative *)
+	  if not (is_empty_univ lev) & not (is_base_univ lev) then
+	    error "Large non-propositional inductive types must be in Type";
+	  Inl (info,full_arity,s)
+      | Prop _ ->
+	  Inl (info,full_arity,s) in
+      (id,cn,lc,(sign,status)))
+      inds ind_min_levels in
+
+  (env_arities, params, inds, cst)
 
 (************************************************************************)
 (************************************************************************)
@@ -477,7 +511,7 @@ let check_positivity env_ar params inds =
     List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in
   let lparams = rel_context_length params in
   let nmr = rel_context_nhyps params in
-  let check_one i (_,_,_,_,_,lc) =
+  let check_one i (_,_,lc,_) =
     let ra_env =
       list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
@@ -509,26 +543,28 @@ let all_sorts = [InProp;InSet;InType]
 let small_sorts = [InProp;InSet]
 let logical_sorts = [InProp]
 
-let allowed_sorts issmall isunit = function
+let allowed_sorts issmall isunit s =
+  match family_of_sort s with
   (* Type: all elimination allowed *)
-  | Type _ -> all_sorts
+  | InType -> all_sorts
 
   (* Small Set is predicative: all elimination allowed *)
-  | Prop Pos when issmall -> all_sorts
+  | InSet when issmall -> all_sorts
 
   (* Large Set is necessarily impredicative: forbids large elimination *)
-  | Prop Pos -> small_sorts
+  | InSet -> small_sorts
 
   (* Unitary/empty Prop: elimination to all sorts are realizable *)
   (* unless the type is large. If it is large, forbids large elimination *)
   (* which otherwise allows to simulate the inconsistent system Type:Type *)
-  | Prop Null when isunit -> if issmall then all_sorts else small_sorts
+  | InProp when isunit -> if issmall then all_sorts else small_sorts
 
   (* Other propositions: elimination only to Prop *)
-  | Prop Null -> logical_sorts
+  | InProp -> logical_sorts
 
 let fold_inductive_blocks f =
-  Array.fold_left (fun acc (_,ar,_,_,_,lc) -> f (Array.fold_left f acc lc) ar)
+  Array.fold_left (fun acc (_,_,lc,(arsign,_)) ->
+    f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (* dummy *) mkSet arsign))
 
 let used_section_variables env inds =
   let ids = fold_inductive_blocks
@@ -542,10 +578,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
   let hyps =  used_section_variables env inds in
   let nparamargs = rel_context_nhyps params in
   (* Check one inductive *)
-  let build_one_packet (id,ar,cnames,issmall,isunit,lc) recarg =
-    (* Arity in normal form *)
-    let (ar_sign,ar_sort) = dest_arity env ar in
-    let nf_ar = if isArity ar then ar else mkArity (ar_sign,ar_sort) in
+  let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
     (* Type of constructors in normal form *)
     let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
     let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
@@ -554,8 +587,19 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
       Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
 	splayed_lc in
     (* Elimination sorts *)
-    let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in
-    let kelim = allowed_sorts issmall isunit ar_sort in
+    let arkind,kelim = match ar_kind with
+    | Inr (param_levels,lev) ->
+	Polymorphic {
+	  mind_param_levels = param_levels;
+	  mind_level = lev; 
+	}, all_sorts
+    | Inl ((issmall,isunit),ar,s) ->
+	let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in
+	let kelim = allowed_sorts issmall isunit s in
+	Monomorphic {
+	  mind_user_arity = ar;
+	  mind_sort = s; 
+	}, kelim in
     let nconst, nblock = ref 0, ref 0 in 
     let transf num =
       let arity = List.length (dest_subterms recarg).(num) in
@@ -571,16 +615,15 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
     let rtbl = Array.init (List.length cnames) transf in
     (* Build the inductive packet *)
     { mind_typename = id;
-      mind_user_arity  = ar;
-      mind_nf_arity = nf_ar;
+      mind_arity = arkind;
+      mind_arity_ctxt = ar_sign;
       mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
-      mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_consnames = Array.of_list cnames;
       mind_consnrealdecls = consnrealargs;
       mind_user_lc = lc;
       mind_nf_lc = nf_lc;
-      mind_recargs = recarg;    
+      mind_recargs = recarg;
       mind_nb_constant = !nconst;
       mind_nb_args = !nblock;
       mind_reloc_tbl = rtbl;
@@ -608,5 +651,5 @@ let check_inductive env mie =
   (* Then check positivity conditions *)
   let (nmr,recargs) = check_positivity env_ar params inds in
   (* Build the inductive packets *)
-  build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite 
+  build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
     inds nmr recargs cst
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 7896b170a..efae466f8 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -47,6 +47,8 @@ let find_coinductive env c =
         when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
     | _ -> raise Not_found
 
+let inductive_params (mib,_) = mib.mind_nparams
+
 (************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)
@@ -80,10 +82,12 @@ let instantiate_params full t args sign =
 
 let instantiate_partial_params = instantiate_params false
 
-let full_inductive_instantiate mib params t =
-  instantiate_params true t params mib.mind_params_ctxt
+let full_inductive_instantiate mib params sign =
+  let dummy = mk_Prop in
+  let t = mkArity (sign,dummy) in
+  fst (destArity (instantiate_params true t params mib.mind_params_ctxt))
 
-let full_constructor_instantiate (((mind,_),mib,_),params) =
+let full_constructor_instantiate ((mind,_),(mib,_),params) =
   let inst_ind = constructor_instantiate mind mib in
   (fun t ->
     instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
@@ -93,22 +97,6 @@ let full_constructor_instantiate (((mind,_),mib,_),params) =
 
 (* Functions to build standard types related to inductive *)
 
-(* For each inductive type of a block that is of level u_i, we have
-   the constraints that u_i >= v_i where v_i is the type level of the
-   types of the constructors of this inductive type. Each v_i depends
-   of some of the u_i and of an extra (maybe non variable) universe,
-   say w_i. Typically, for three inductive types, we could have
-
-   u1,u2,u3,w1 <= u1
-   u1       w2 <= u2
-      u2,u3,w3 <= u3
-
-   From this system of inequations, we shall deduce
-
-   w1,w2,w3 <= u1
-   w1,w2 <= u2
-   w1,w2,w3 <= u3
-*)   
 
 let number_of_inductives mib = Array.length mib.mind_packets
 let number_of_constructors mip = Array.length mip.mind_consnames
@@ -134,17 +122,6 @@ where
 Remark: Set (predicative) is encoded as Type(0)
 *)
 
-let find_constraint levels level_bounds i nci =
-  if nci = 0 then mk_Prop
-  else
-    let level_bounds' = solve_constraints_system levels level_bounds in
-    let level = level_bounds'.(i) in
-    if nci = 1 & is_empty_universe level then mk_Prop
-    else if Univ.is_base level then mk_Set else Type level
-
-let find_inductive_level env (mib,mip) (_,i) levels level_bounds =
-  find_constraint levels level_bounds i (number_of_constructors mip)
-
 let set_inductive_level env s t = 
   let sign,s' = dest_prod_assum env t in
   if family_of_sort s <> family_of_sort (destSort s') then
@@ -153,45 +130,69 @@ let set_inductive_level env s t =
   else
     t
 
-let constructor_instances env (mib,mip) (_,i) args =
-  let nargs = Array.length args in
-  let args = Array.to_list args in
-  let uargs = 
-    if nargs > mib.mind_nparams_rec then
-      fst (list_chop mib.mind_nparams_rec args)
-    else args in
-  let arities =
-    Array.map (fun mip -> destArity mip.mind_nf_arity) mib.mind_packets in
-  (* Compute the minimal type *)
-  let levels = Array.init 
-    (number_of_inductives mib) (fun _ -> fresh_local_univ ()) in
-  let arities = list_tabulate (fun i -> 
-    let ctx,s = arities.(i) in
-    let s = match s with Type _ -> Type (levels.(i)) | s -> s in
-    (Name mib.mind_packets.(i).mind_typename,None,mkArity (ctx,s)))
-    (number_of_inductives mib) in
-             (* Remark: all arities are closed hence no need for lift *)
-  let env_ar = push_rel_context (List.rev arities) env in
-  let uargs = List.map (lift (number_of_inductives mib)) uargs in
-  let lc =
-    Array.map (fun mip ->
-        Array.map (fun c -> 
-	    instantiate_partial_params c uargs mib.mind_params_ctxt)
-          mip.mind_nf_lc)
-      mib.mind_packets in
-  env_ar, lc, levels
-
-let is_small_inductive (mip,mib) = is_small (snd (destArity mib.mind_nf_arity))
-
-let max_inductive_sort v =
-  let v = Array.map (function
-    | Type u -> u
-    | _ -> anomaly "Only type levels when computing the minimal sort of an inductive type") v in
-  Univ.sup_array v
-
-(* Type of an inductive type *)
-
-let type_of_inductive (_,mip) = mip.mind_user_arity
+let sort_as_univ = function
+| Type u -> u
+| Prop Null -> neutral_univ
+| Prop Pos -> base_univ
+
+let rec make_subst env exp act =
+  match exp, act with
+  (* Bind expected levels of parameters to actual levels *)
+  | None :: exp, _ :: act ->
+      make_subst env exp act
+  | Some u :: exp, t :: act -> 
+      (u, sort_as_univ (snd (dest_arity env t))) :: make_subst env exp act
+  (* Not enough parameters, create a fresh univ *)
+  | Some u :: exp, [] ->
+      (u, fresh_local_univ ()) :: make_subst env exp []
+  | None :: exp, [] ->
+      make_subst env exp []
+  (* Uniform parameters are exhausted *)
+  | [], _ -> []
+
+let sort_of_instantiated_universe mip subst level =
+  let level = subst_large_constraints subst level in
+  let nci = number_of_constructors mip in
+  if nci = 0 then mk_Prop
+  else
+    if is_empty_univ level then if nci = 1 then mk_Prop else mk_Set 
+    else if is_base_univ level then mk_Set
+    else Type level
+
+let instantiate_inductive_with_param_levels env ar mip paramtyps =
+  let args = Array.to_list paramtyps in
+  let subst = make_subst env ar.mind_param_levels args in
+  sort_of_instantiated_universe mip subst ar.mind_level
+
+let type_of_applied_inductive env mip paramtyps =
+  match mip.mind_arity with
+  | Monomorphic s ->
+      s.mind_user_arity
+  | Polymorphic ar ->
+      let s = instantiate_inductive_with_param_levels env ar mip paramtyps in
+      mkArity (mip.mind_arity_ctxt,s)
+
+(* The max of an array of universes *)
+
+let cumulate_constructor_univ u = function
+  | Prop Null -> u
+  | Prop Pos -> sup base_univ u
+  | Type u' -> sup u u'
+
+let max_inductive_sort =
+  Array.fold_left cumulate_constructor_univ neutral_univ
+
+(* Type of a (non applied) inductive type *)
+
+let type_of_inductive (_,mip) =
+  match mip.mind_arity with
+  | Monomorphic s -> s.mind_user_arity
+  | Polymorphic s ->
+      let subst = map_succeed (function
+	| Some u -> (u, fresh_local_univ ())
+	| None -> failwith "") s.mind_param_levels in
+      let s = mkSort (sort_of_instantiated_universe mip subst s.mind_level) in
+      it_mkProd_or_LetIn s mip.mind_arity_ctxt
 
 (************************************************************************)
 (* Type of a constructor *)
@@ -215,19 +216,11 @@ let arities_of_constructors ind specif =
 
 (************************************************************************)
 
-let is_info_arity env c =
-  match dest_arity env c with
-    | (_,Prop Null) -> false 
-    | (_,Prop Pos)  -> true 
-    | (_,Type _)    -> true
-
-let error_elim_expln env kp ki =
-  if is_info_arity env kp && not (is_info_arity env ki) then
-    NonInformativeToInformative
-  else 
-    match (kind_of_term kp,kind_of_term ki) with 
-      | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType
-      | _ -> WrongArity
+let error_elim_expln kp ki =
+  match kp,ki with
+  | (InType | InSet), InProp -> NonInformativeToInformative
+  | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
+  | _ -> WrongArity
 
 (* Type of case predicates *)
 
@@ -244,9 +237,20 @@ let local_rels ctxt =
   rels
 
 (* Get type of inductive, with parameters instantiated *)
-let get_arity mib mip params =
-  let arity = mip.mind_nf_arity in
-  destArity (full_inductive_instantiate mib params arity)
+
+let inductive_sort_family mip =
+  match mip.mind_arity with
+   | Monomorphic s -> family_of_sort s.mind_sort 
+   | Polymorphic _ -> InType
+
+let mind_arity mip =
+  mip.mind_arity_ctxt, inductive_sort_family mip
+
+let get_instantiated_arity (mib,mip) params =
+  let sign, s = mind_arity mip in
+  full_inductive_instantiate mib params sign, s
+
+let elim_sorts (_,mip) = mip.mind_kelim
 
 let rel_list n m = 
   let rec reln l p = 
@@ -254,66 +258,48 @@ let rel_list n m =
   in 
   reln [] 1
 
-let build_dependent_inductive ind mib mip params =
+let build_dependent_inductive ind (_,mip) params =
   let nrealargs = mip.mind_nrealargs in
   applist 
     (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
 
-
 (* This exception is local *)
-exception LocalArity of (constr * constr * arity_error) option
+exception LocalArity of (sorts_family * sorts_family * arity_error) option
 
-let is_correct_arity env c pj ind mib mip params = 
-  let kelim = mip.mind_kelim in
-  let arsign,s = get_arity mib mip params in
-  let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
-  let rec srec env pt t u =
+let check_allowed_sort ksort specif =
+  if not (List.exists ((=) ksort) (elim_sorts specif)) then 
+    let s = inductive_sort_family (snd specif) in
+    raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
+
+let is_correct_arity env c pj ind specif params = 
+  let arsign,_ = get_instantiated_arity specif params in
+  let rec srec env pt ar u =
     let pt' = whd_betadeltaiota env pt in
-    let t' = whd_betadeltaiota env t in
-    match kind_of_term pt', kind_of_term t' with
-      | Prod (na1,a1,a2), Prod (_,a1',a2') ->
+    match kind_of_term pt', ar with
+      | Prod (na1,a1,t), (_,None,a1')::ar' ->
           let univ =
             try conv env a1 a1'
             with NotConvertible -> raise (LocalArity None) in
-          srec (push_rel (na1,None,a1) env) a2 a2' (Constraint.union u univ)
-      | Prod (_,a1,a2), _ -> (* whnf of t was not needed here! *)
-          let k = whd_betadeltaiota env a2 in 
-          let ksort = match kind_of_term k with
+          srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ)
+      | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
+          let ksort = match kind_of_term (whd_betadeltaiota env a2) with
             | Sort s -> family_of_sort s 
 	    | _ -> raise (LocalArity None) in
-
-	  let dep_ind = build_dependent_inductive ind mib mip params
-	  in 
+	  let dep_ind = build_dependent_inductive ind specif params in 
           let univ =
             try conv env a1 dep_ind
             with NotConvertible -> raise (LocalArity None) in
-          if List.exists ((=) ksort) kelim then
-	    (true, Constraint.union u univ)
-          else 
-	    raise (LocalArity (Some(k,t',error_elim_expln env k t')))
-      | k, Prod (_,_,_) ->
+	  check_allowed_sort ksort specif;
+	  (true, Constraint.union u univ)
+      | Sort s', [] ->
+	  check_allowed_sort (family_of_sort s') specif;
+	  (false, u)
+      | _ ->
 	  raise (LocalArity None)
-      | k, ki -> 
-	  let ksort = match k with
-            | Sort s -> family_of_sort s 
-            | _ ->  raise (LocalArity None) in
-          if List.exists ((=) ksort) kelim then 
-	    (false, u)
-          else 
-	    raise (LocalArity (Some(pt',t',error_elim_expln env pt' t')))
   in 
-  try srec env pj.uj_type nodep_ar Constraint.empty
+  try srec env pj.uj_type (List.rev arsign) Constraint.empty
   with LocalArity kinds ->
-    let create_sort = function 
-      | InProp -> mkProp
-      | InSet -> mkSet
-      | InType -> mkSort type_0 in
-    let listarity = List.map create_sort kelim
-(*    let listarity =
-      (List.map (fun s -> make_arity env true indf (create_sort s)) kelim)
-      @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim)*)
-    in 
-    error_elim_arity env ind listarity c pj kinds
+    error_elim_arity env ind (elim_sorts specif) c pj kinds
 
 
 (************************************************************************)
@@ -321,13 +307,13 @@ let is_correct_arity env c pj ind mib mip params =
 
 (* [p] is the predicate, [i] is the constructor number (starting from 0),
    and [cty] is the type of the constructor (params not instantiated) *)
-let build_branches_type ind mib mip params dep p =
+let build_branches_type ind (_,mip as specif) params dep p =
   let build_one_branch i cty =
-    let typi = full_constructor_instantiate ((ind,mib,mip),params) cty in
+    let typi = full_constructor_instantiate (ind,specif,params) cty in
     let (args,ccl) = decompose_prod_assum typi in
     let nargs = rel_context_length args in
     let (_,allargs) = decompose_app ccl in
-    let (lparams,vargs) = list_chop mib.mind_nparams allargs in
+    let (lparams,vargs) = list_chop (inductive_params specif) allargs in
     let cargs =
       if dep then
         let cstr = ith_constructor_of_inductive ind (i+1) in
@@ -346,12 +332,12 @@ let build_case_type dep p c realargs =
   beta_appvect p (Array.of_list args)
 
 let type_case_branches env (ind,largs) pj c =
-  let (mib,mip) = lookup_mind_specif env ind in 
-  let nparams = mib.mind_nparams in
+  let specif = lookup_mind_specif env ind in 
+  let nparams = inductive_params specif in
   let (params,realargs) = list_chop nparams largs in
   let p = pj.uj_val in
-  let (dep,univ) = is_correct_arity env c pj ind mib mip params in
-  let lc = build_branches_type ind mib mip params dep p in
+  let (dep,univ) = is_correct_arity env c pj ind specif params in
+  let lc = build_branches_type ind specif params dep p in
   let ty = build_case_type dep p c realargs in
   (lc, ty, univ)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index b4adbf093..c0a138bde 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -38,6 +38,8 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 
 val type_of_inductive : mind_specif -> types
 
+val elim_sorts : mind_specif -> sorts_family list
+
 (* Return type as quoted by the user *)
 val type_of_constructor : constructor -> mind_specif -> types
 
@@ -58,6 +60,11 @@ val type_case_branches :
   env -> inductive * constr list -> unsafe_judgment -> constr
     -> types array * types * constraints
 
+(* Return the arity of an inductive type *)
+val mind_arity : one_inductive_body -> Sign.rel_context * sorts_family
+
+val inductive_sort_family : one_inductive_body -> sorts_family
+
 (* Check a [case_info] actually correspond to a Case expression on the
    given inductive type. *)
 val check_case_info : env -> inductive -> case_info -> unit
@@ -68,16 +75,11 @@ val check_cofix : env -> cofixpoint -> unit
 
 (*s Support for sort-polymorphic inductive types *)
 
-val constructor_instances : env -> mind_specif -> inductive -> 
-  constr array -> env * types array array * universe array
+val type_of_applied_inductive :
+  env -> one_inductive_body -> types array -> types
 
 val set_inductive_level : env -> sorts -> types -> types
 
-val find_inductive_level : env -> mind_specif -> inductive -> 
-  universe array -> universe array -> sorts
-
-val is_small_inductive : mind_specif -> bool
-
 val max_inductive_sort : sorts array -> universe
 
 (***************************************************************)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index e72942608..5b69ac7b6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -438,7 +438,7 @@ let dest_prod_assum env =
   prodec_rec env Sign.empty_rel_context
 
 let dest_arity env c =
-  let l, c = dest_prod env c in
+  let l, c = dest_prod_assum env c in
   match kind_of_term c with
     | Sort s -> l,s
     | _ -> error "not an arity"
diff --git a/kernel/sign.ml b/kernel/sign.ml
index dbf52498d..52af09b5a 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -191,3 +191,4 @@ let decompose_lam_n_assum n =
     | c -> error "decompose_lam_n_assum: not enough abstractions"
   in 
   lamdec_rec empty_rel_context n 
+
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 0c339e8b8..6de7819af 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -89,14 +89,15 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       (* nf_arity later *)
       (* user_lc ignored *)
       (* user_arity ignored *)
-      let cst = check_conv cst conv_sort env p1.mind_sort p2.mind_sort in
       check (fun p -> p.mind_nrealargs);
       (* kelim ignored *)
       (* listrec ignored *)
       (* finite done *)
       (* nparams done *)
       (* params_ctxt done *)
-      let cst = check_conv cst conv env p1.mind_nf_arity p2.mind_nf_arity in
+      (* Don't check the sort of the type if polymorphic *)
+      let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2))
+      in
 	cst
   in
   let check_cons_types i cst p1 p2 =
@@ -181,7 +182,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
        "name.") ;
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if cb2.const_body <> None then error () ;
-      let arity1 = mind1.mind_packets.(i).mind_user_arity in
+      let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in
        check_conv cst conv_leq env arity1 cb2.const_type
    | IndConstr (((kn,i),j) as cstr,mind1) ->
       Util.error ("The kernel does not recognize yet that a parameter can be " ^
diff --git a/kernel/term.ml b/kernel/term.ml
index 87c319a1b..f59a6c183 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -769,17 +769,16 @@ let substkey = Profile.declare_profile "substn_many";;
 let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
 *)
 
-let substnl laml k =
-  substn_many (Array.map make_substituend (Array.of_list laml)) k
-let substl laml =
-  substn_many (Array.map make_substituend (Array.of_list laml)) 0
+let substnl laml n =
+  substn_many (Array.map make_substituend (Array.of_list laml)) n
+let substl laml = substnl laml 0
 let subst1 lam = substl [lam]
 
-let substl_decl laml (id,bodyopt,typ) =
-  match bodyopt with
-    | None -> (id,None,substl laml typ)
-    | Some body -> (id, Some (substl laml body), type_app (substl laml) typ)
+let substnl_decl laml k (id,bodyopt,typ) =
+  (id,option_map (substnl laml k) bodyopt,substnl laml k typ)
+let substl_decl laml = substnl_decl laml 0
 let subst1_decl lam = substl_decl [lam]
+let subst1_named_decl = subst1_decl
 
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 160ef767b..0982ee456 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -460,8 +460,11 @@ val substnl : constr list -> int -> constr -> constr
 val substl : constr list -> constr -> constr
 val subst1 : constr -> constr -> constr
 
-val substl_decl : constr list -> named_declaration -> named_declaration
-val subst1_decl : constr -> named_declaration -> named_declaration
+val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration
+val substl_decl : constr list -> rel_declaration -> rel_declaration
+val subst1_decl : constr -> rel_declaration -> rel_declaration
+
+val subst1_named_decl : constr -> named_declaration -> named_declaration
 
 val replace_vars : (identifier * constr) list -> constr -> constr
 val subst_var : identifier -> constr -> constr
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 7049a8afe..bbd3e4bf4 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -45,8 +45,8 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
-  | ElimArity of inductive * types list * constr * unsafe_judgment
-      * (constr * constr * arity_error) option
+  | ElimArity of inductive * sorts_family list * constr * unsafe_judgment
+      * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of unsafe_judgment
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index ffa16968c..6e480479e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -47,8 +47,8 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
-  | ElimArity of inductive * types list * constr * unsafe_judgment
-      * (constr * constr * arity_error) option
+  | ElimArity of inductive * sorts_family list * constr * unsafe_judgment
+      * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of unsafe_judgment
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
@@ -75,8 +75,8 @@ val error_assumption : env -> unsafe_judgment -> 'a
 val error_reference_variables : env -> constr -> 'a
 
 val error_elim_arity : 
-  env -> inductive -> types list -> constr 
-    -> unsafe_judgment -> (constr * constr * arity_error) option -> 'a
+  env -> inductive -> sorts_family list -> constr -> unsafe_judgment -> 
+      (sorts_family * sorts_family * arity_error) option -> 'a
 
 val error_case_not_inductive : env -> unsafe_judgment -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 29ec5007a..435b3e31c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -245,14 +245,16 @@ let judge_of_cast env cj k tj =
 
 (* Inductive types. *)
 
-let judge_of_inductive env i =
-  let constr = mkInd i in
-  let _ =
-    let (kn,_) = i in
-    let mib = lookup_mind kn env in
-    check_args env constr mib.mind_hyps in 
-  let specif = lookup_mind_specif env i in
-  make_judge constr (type_of_inductive specif)
+let judge_of_applied_inductive env ind jl =
+  let c = mkInd ind in
+  let (mib,mip) = lookup_mind_specif env ind in
+  check_args env c mib.mind_hyps;
+  let paramstyp = Array.map (fun j -> j.uj_type) jl in
+  let t = Inductive.type_of_applied_inductive env mip paramstyp in
+  make_judge c t
+
+let judge_of_inductive env ind =
+  judge_of_applied_inductive env ind [||]
 
 (* Constructors. *)
 
@@ -334,14 +336,15 @@ let rec execute env cstr cu =
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-	let (j,cu1) = execute env f cu in
-        let (jl,cu2) = execute_array env args cu1 in
-	let (j',cu) = univ_combinator cu2 (judge_of_apply env j jl) in
-	if isInd f then
-	  (* Sort-polymorphism of inductive types *)
-	  adjust_inductive_level env (destInd f) args (j',cu)
-	else
-	  (j',cu)
+        let (jl,cu1) = execute_array env args cu in
+	let (j,cu2) =
+	  if isInd f then
+	    (* Sort-polymorphism of inductive types *)
+	    judge_of_applied_inductive env (destInd f) jl, cu1
+	  else
+	    execute env f cu1
+	in
+	univ_combinator cu2 (judge_of_apply env j jl)
 	    
     | Lambda (name,c1,c2) -> 
         let (varj,cu1) = execute_type env c1 cu in
@@ -421,22 +424,6 @@ and execute_array env = array_fold_map' (execute env)
 
 and execute_list env = list_fold_map' (execute env) 
 
-and adjust_inductive_level env ind args (j,cu) =
-  let specif = lookup_mind_specif env ind in
-  if is_small_inductive specif then
-    (* No polymorphism *)
-    (j,cu)
-  else
-    (* Retyping constructor with the actual arguments *)
-    let env',llc,ls0 = constructor_instances env specif ind args in
-    let (llj,cu1) = array_fold_map' (execute_array env') llc cu in
-    let ls =
-      Array.map (fun lj ->
-	max_inductive_sort (Array.map (sort_judgment env) lj)) llj
-    in
-    let s = find_inductive_level env specif ind ls0 ls in
-    (on_judgment_type (set_inductive_level env s) j, cu1)
-
 (* Derived functions *)
 let infer env constr =
   let (j,(cst,_)) =
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 412998f6e..25f7d15db 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -78,6 +78,9 @@ val judge_of_cast :
 
 val judge_of_inductive : env -> inductive -> unsafe_judgment
 
+val judge_of_applied_inductive : 
+  env -> inductive -> unsafe_judgment array -> unsafe_judgment
+
 val judge_of_constructor : env -> constructor -> unsafe_judgment
 
 (*s Type of Cases. *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1e0991e3d..906354b04 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -8,6 +8,10 @@
 
 (* $Id$ *)
 
+(* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
+(* Extension with algebraic universes by HH [Sep 2001] *)
+(* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *)
+
 (* Universes are stratified by a partial ordering $\le$.
    Let $\~{}$ be the associated equivalence. We also have a strict ordering
    $<$ between equivalence classes, and we maintain that $<$ is acyclic,
@@ -92,7 +96,7 @@ let sup u v =
 	let gtl'' = list_union gtl gtl' in
 	Max (list_subtract gel'' gtl'',gtl'')
 
-let sup_array ls = Array.fold_right sup ls (Max ([],[]))
+let neutral_univ = Max ([],[])
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
@@ -125,7 +129,7 @@ let declare_univ u g =
 (* The level of Set *)
 let base_univ = Atom Base
 
-let is_base = function
+let is_base_univ = function
   | Atom Base -> true
   | Max ([Base],[]) -> warning "Non canonical Set"; true
   | u -> false
@@ -428,11 +432,11 @@ let make_max = function
   | ([u],[]) -> Atom u
   | (le,lt) -> Max (le,lt)
 
-let remove_constraint u = function
+let remove_large_constraint u = function
   | Atom u' as x -> if u = u' then Max ([],[]) else x
   | Max (le,lt) -> make_max (list_remove u le,lt)
 
-let is_empty_universe = function
+let is_empty_univ = function
   | Max ([],[]) -> true
   | _ -> false
 
@@ -454,22 +458,40 @@ where
   - the wi are arbitrary complex universes that do not mention the ui.
 *)
 
+let is_direct_sort_constraint s v = match s with
+  | Some u -> is_direct_constraint u v
+  | None -> false
+
 let solve_constraints_system levels level_bounds =
   let levels = 
-    Array.map (function Atom u -> u | _ -> anomaly "expects Atom") levels in
+    Array.map (option_map (function Atom u -> u | _ -> anomaly "expects Atom"))
+      levels in
   let v = Array.copy level_bounds in
   let nind = Array.length v in
   for i=0 to nind-1 do
     for j=0 to nind-1 do
-      if i<>j & is_direct_constraint levels.(j) v.(i) then
-	v.(i) <- sup v.(i) v.(j)
+      if i<>j & is_direct_sort_constraint levels.(j) v.(i) then
+	v.(i) <- sup v.(i) level_bounds.(j)
     done;
     for j=0 to nind-1 do
-      v.(i) <- remove_constraint levels.(j) v.(i)
+      match levels.(j) with
+      | Some u -> v.(i) <- remove_large_constraint u v.(i)
+      | None -> ()
     done
   done;
   v
 
+let subst_large_constraint u u' v =
+  match u with 
+  | Atom u ->
+      if is_direct_constraint u v then sup u' (remove_large_constraint u v)
+      else v
+  | _ ->
+      anomaly "expect a universe level"
+
+let subst_large_constraints =
+  List.fold_right (fun (u,u') -> subst_large_constraint u u')
+
 (* Pretty-printing *)
 
 let num_universes g =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 0fb1a4ca8..a7d27f47c 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -14,9 +14,10 @@ type universe
 
 val base_univ : universe
 val prop_univ : universe
+val neutral_univ : universe
 val make_univ : Names.dir_path * int -> universe
 
-val is_base : universe -> bool
+val is_base_univ : universe -> bool
 
 (* The type of a universe *)
 val super : universe -> universe
@@ -24,9 +25,6 @@ val super : universe -> universe
 (* The max of 2 universes *)
 val sup   : universe -> universe -> universe
 
-(* The max of an array of universes *)
-val sup_array : universe array -> universe
-
 (*s Graphs of universes. *)
 
 type universes
@@ -58,10 +56,15 @@ val merge_constraints : constraints -> universes -> universes
 
 val fresh_local_univ : unit -> universe
 
-val solve_constraints_system : universe array -> universe array -> 
+val solve_constraints_system : universe option array -> universe array -> 
   universe array
 
-val is_empty_universe : universe -> bool
+val is_empty_univ : universe -> bool
+
+val subst_large_constraint : universe -> universe -> universe -> universe
+
+val subst_large_constraints : 
+  (universe * universe) list -> universe -> universe
 
 (*s Pretty-printing of universes. *)
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index f038c04f1..653f8978c 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -342,8 +342,8 @@ let constr_type_of_idkey env idkey =
       mkRel n, lift n ty
 
 let type_of_ind env ind = 
-  let (_,mip) = Inductive.lookup_mind_specif env ind in
-  mip.mind_nf_arity
+  let specif = Inductive.lookup_mind_specif env ind in
+  Inductive.type_of_inductive specif
 
 let build_branches_type (mind,_ as _ind) mib mip params dep p rtbl =
   (* [build_one_branch i cty] construit le type de la ieme branche (commence
@@ -461,7 +461,8 @@ and nf_stk env c t stk  =
 	in 
 	let aux = 
 	  nf_predicate env (type_of_switch sw) 
-	    (hnf_prod_applist env mip.mind_nf_arity (Array.to_list params)) in
+	    (hnf_prod_applist env (type_of_ind env ind) (Array.to_list params))
+	in
 	!dep,aux in
       (* Calcul du type des branches *)
       let btypes =