Adapt the checker to polymorphic universes and projections (untested).

21 files changed, 793 insertions, 216 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index b9009da82..f3c583b83 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -297,7 +297,8 @@ let rec explain_exn = function
           str("\nCantApplyBadType at argument " ^ string_of_int n)
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
-      | IllTypedRecBody _ -> str"IllTypedRecBody"))
+      | IllTypedRecBody _ -> str"IllTypedRecBody"
+      | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"))
 
   | Indtypes.InductiveError e ->
       hov 0 (str "Error related to inductive types")
diff --git a/checker/cic.mli b/checker/cic.mli
index d2f785abf..484d64973 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -79,6 +79,10 @@ type 'constr pfixpoint =
     (int array * int) * 'constr prec_declaration
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
+type 'a puniverses = 'a Univ.puniverses
+type pconstant = constant puniverses
+type pinductive = inductive puniverses
+type pconstructor = constructor puniverses
 
 type constr =
   | Rel       of int
@@ -91,12 +95,13 @@ type constr =
   | Lambda    of Name.t * constr * constr
   | LetIn     of Name.t * constr * constr * constr
   | App       of constr * constr array
-  | Const     of constant
-  | Ind       of inductive
-  | Construct of constructor
+  | Const     of pconstant
+  | Ind       of pinductive
+  | Construct of pconstructor
   | Case      of case_info * constr * constr * constr array
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
+  | Proj      of constant * constr
 
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
@@ -163,7 +168,17 @@ type engagement = ImpredicativeSet
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
-type constant_type = constr
+
+type template_arity = {
+  template_param_levels : Univ.universe option list;
+  template_level : Univ.universe;
+}
+
+type ('a, 'b) declaration_arity = 
+  | RegularArity of 'a
+  | TemplateArity of 'b
+
+type constant_type = (constr, rel_context * template_arity) declaration_arity
 
 (** Inlining level of parameters at functor applications.
     This is ignored by the checker. *)
@@ -173,11 +188,24 @@ type inline = int option
 (** A constant can have no body (axiom/parameter), or a
     transparent body, or an opaque one *)
 
+(** Projections are a particular kind of constant: 
+    always transparent. *)
+
+type projection_body = {
+  proj_ind : mutual_inductive;
+  proj_npars : int;
+  proj_arg : int;
+  proj_type : constr; (* Type under params *)
+  proj_body : constr; (* For compatibility, the match version *)
+}
+
 type constant_def =
   | Undef of inline
   | Def of constr_substituted
   | OpaqueDef of lazy_constr
 
+type constant_universes = Univ.universe_context
+
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constant_def;
@@ -185,6 +213,9 @@ type constant_body = {
     const_body_code : to_patch_substituted;
     const_constraints : Univ.constraints;
     const_native_name : native_name ref;
+    const_polymorphic : bool; (** Is it polymorphic or not *)
+    const_universes : constant_universes;
+    const_proj : projection_body option;
     const_inline_code : bool }
 
 (** {6 Representation of mutual inductive types } *)
@@ -196,6 +227,13 @@ type recarg =
 
 type wf_paths = recarg Rtree.t
 
+type regular_inductive_arity = {
+  mind_user_arity : constr;
+  mind_sort : sorts;
+}
+
+type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
+
 type one_inductive_body = {
 (** {8 Primitive datas } *)
 
@@ -203,7 +241,7 @@ type one_inductive_body = {
 
     mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
 
-    mind_arity : constr; (** Arity sort and original user arity if monomorphic *)
+    mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *)
 
     mind_consnames : Id.t array; (** Names of the constructors: [cij] *)
 
@@ -245,7 +283,9 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : bool;  (** Whether the inductive type has been declared as a record *)
+    mind_record : (constr * constant array) option;  
+    (** Whether the inductive type has been declared as a record, 
+	In that case we get its canonical eta-expansion and list of projections. *)
 
     mind_finite : bool;  (** Whether the type is inductive or coinductive *)
 
@@ -259,7 +299,11 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_constraints : Univ.constraints;  (** Universes constraints enforced by the inductive declaration *)
+    mind_polymorphic : bool; (** Is it polymorphic or not *)
+
+    mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
+
+    mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
 (** {8 Data for native compilation } *)
 
diff --git a/checker/closure.ml b/checker/closure.ml
index 831f50454..5bd636b16 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -160,16 +160,19 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
  * instantiations (cbv or lazy) are.
  *)
 
-type table_key =
-  | ConstKey of constant
+type 'a tableKey =
+  | ConstKey of 'a
   | VarKey of Id.t
   | RelKey of int
 
+type table_key = constant puniverses tableKey
+
 module KeyHash =
 struct
   type t = table_key
   let equal k1 k2 = match k1, k2 with
-  | ConstKey c1, ConstKey c2 -> Constant.UserOrd.equal c1 c2
+  | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2 
+    && Univ.Instance.equal u1 u2
   | VarKey id1, VarKey id2 -> Id.equal id1 id2
   | RelKey i1, RelKey i2 -> Int.equal i1 i2
   | (ConstKey _ | VarKey _ | RelKey _), _ -> false
@@ -177,7 +180,7 @@ struct
   open Hashset.Combine
 
   let hash = function
-  | ConstKey c -> combinesmall 1 (Constant.UserOrd.hash c)
+  | ConstKey (c,u) -> combinesmall 1 (Constant.UserOrd.hash c)
   | VarKey id -> combinesmall 2 (Id.hash id)
   | RelKey i -> combinesmall 3 (Int.hash i)
 end
@@ -223,10 +226,7 @@ let defined_rels flags env =
 
 let mind_equiv_infos info = mind_equiv info.i_env
 
-let eq_table_key k1 k2 = 
- match k1,k2 with
-   | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2
-   | _,_  -> k1=k2
+let eq_table_key = KeyHash.equal
 
 let create mk_cl flgs env =
   { i_flags = flgs;
@@ -273,9 +273,10 @@ and fterm =
   | FAtom of constr (* Metas and Sorts *)
   | FCast of fconstr * cast_kind * fconstr
   | FFlex of table_key
-  | FInd of inductive
-  | FConstruct of constructor
+  | FInd of pinductive
+  | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
+  | FProj of constant * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCases of case_info * fconstr * fconstr * fconstr array
@@ -305,6 +306,7 @@ let update v1 (no,t) =
 type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
+  | Zproj of int * int * constant
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -390,6 +392,9 @@ let rec compact_constr (lg, subs as s) c k =
         let (f',s) = compact_constr s f k in
         let (v',s) = compact_vect s v k in
         if f==f' && v==v' then c,s else App(f',v'), s
+    | Proj (p, t) -> 
+        let (t', s) = compact_constr s t k in
+	  if t' == t then c,s else Proj(p,t'), s
     | Lambda(n,a,b) ->
         let (a',s) = compact_constr s a k in
         let (b',s) = compact_constr s b (k+1) in
@@ -459,7 +464,7 @@ let mk_clos e t =
     | Meta _ | Sort _ ->  { norm = Norm; term = FAtom t }
     | Ind kn -> { norm = Norm; term = FInd kn }
     | Construct kn -> { norm = Cstr; term = FConstruct kn }
-    | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _) ->
+    | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
         {norm = Red; term = FCLOS(t,e)}
 
 let mk_clos_vect env v = Array.map (mk_clos env) v
@@ -478,6 +483,9 @@ let mk_clos_deep clos_fun env t =
     | App (f,v) ->
         { norm = Red;
 	  term = FApp (clos_fun env f, Array.map (clos_fun env) v) }
+    | Proj (p,c) ->
+	{ norm = Red;
+	  term = FProj (p, clos_fun env c) }
     | Case (ci,p,c,v) ->
         { norm = Red;
 	  term = FCases (ci, clos_fun env p, clos_fun env c,
@@ -533,6 +541,8 @@ let rec to_constr constr_fun lfts v =
     | FApp (f,ve) ->
 	App (constr_fun lfts f,
 	       Array.map (constr_fun lfts) ve)
+    | FProj (p,c) ->
+        Proj (p,constr_fun lfts c)
     | FLambda _ ->
         let (na,ty,bd) = destFLambda mk_clos2 v in
 	Lambda (na, constr_fun lfts ty,
@@ -584,6 +594,8 @@ let rec zip m stk =
     | Zcase(ci,p,br)::s ->
         let t = FCases(ci, p, m, br) in
         zip {norm=neutr m.norm; term=t} s
+    | Zproj (i,j,cst) :: s -> 
+        zip {norm=neutr m.norm; term=FProj (cst,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
     | Zshift(n)::s ->
@@ -660,7 +672,7 @@ let rec get_args n tys f e stk =
 
 (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
 let rec eta_expand_stack = function
-  | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s ->
+  | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ | Zproj _ as e) :: s ->
       e :: eta_expand_stack s
   | [] ->
       [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
@@ -690,6 +702,65 @@ let rec drop_parameters depth n stk =
     | [] -> assert (n=0); []
     | _ -> assert false (* we know that n < stack_args_size(stk) *)
 
+(** Projections and eta expansion *)
+
+let rec get_parameters depth n argstk =
+  match argstk with
+      Zapp args::s ->
+        let q = Array.length args in
+        if n > q then Array.append args (get_parameters depth (n-q) s)
+        else if Int.equal n q then [||]
+        else Array.sub args 0 n
+    | Zshift(k)::s -> 
+      get_parameters (depth-k) n s
+    | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
+	if Int.equal n 0 then [||]
+	else raise Not_found (* Trying to eta-expand a partial application..., should do 
+				eta expansion first? *)
+    | _ -> assert false
+	(* strip_update_shift_app only produces Zapp and Zshift items *)
+
+let eta_expand_ind_stack env lft (ind,u) m s (lft, h) =
+  let mib = lookup_mind (fst ind) env in
+    match mib.mind_record with
+    | None -> raise Not_found
+    | Some (exp,_) -> 
+      let pars = mib.mind_nparams in
+      let h' = fapp_stack h in
+      let (depth, args, _) = strip_update_shift_app m s in
+      let paramargs = get_parameters depth pars args in
+      let subs = subs_cons (Array.append paramargs [|h'|], subs_id 0) in
+      let fexp = mk_clos subs exp in
+	(lft, (fexp, []))
+
+let eta_expand_ind_stacks env ind m s h =
+  let mib = lookup_mind (fst ind) env in
+    match mib.mind_record with
+    | Some (exp,projs) when Array.length projs > 0 -> 
+      let pars = mib.mind_nparams in
+      let h' = fapp_stack h in
+      let (depth, args, _) = strip_update_shift_app m s in
+      let primitive = Environ.is_projection projs.(0) env in
+	if primitive then
+	  let s' = drop_parameters depth pars args in
+      (* Construct, pars1 .. parsm :: arg1...argn :: s ~= (t, []) ->
+	 arg1..argn :: s ~= (proj1 t...projn t) s
+      *)
+	  let hstack = Array.map (fun p -> { norm = Red;
+					     term = FProj (p, h') }) projs in
+	    s', [Zapp hstack]
+	else raise Not_found (* disallow eta-exp for non-primitive records *)
+    | _ -> raise Not_found
+
+let rec project_nth_arg n argstk =
+  match argstk with
+  | Zapp args :: s -> 
+      let q = Array.length args in
+	if n >= q then project_nth_arg (n - q) s
+	else (* n < q *) args.(n)
+  | _ -> assert false
+      (* After drop_parameters we have a purely applicative stack *)
+
 
 (* Iota reduction: expansion of a fixpoint.
  * Given a fixpoint and a substitution, returns the corresponding
@@ -721,33 +792,44 @@ let contract_fix_vect fix =
    atom or a subterm that may produce a redex (abstraction,
    constructor, cofix, letin, constant), or a neutral term (product,
    inductive) *)
-let rec knh m stk =
+let rec knh info m stk =
   match m.term with
-    | FLIFT(k,a) -> knh a (zshift k stk)
-    | FCLOS(t,e) -> knht e t (zupdate m stk)
+    | FLIFT(k,a) -> knh info a (zshift k stk)
+    | FCLOS(t,e) -> knht info e t (zupdate m stk)
     | FLOCKED -> assert false
-    | FApp(a,b) -> knh a (append_stack b (zupdate m stk))
-    | FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk)
+    | FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
+    | FCases(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
     | FFix(((ri,n),(_,_,_)),_) ->
         (match get_nth_arg m ri.(n) stk with
-             (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk')
+             (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
            | (None, stk') -> (m,stk'))
-    | FCast(t,_,_) -> knh t stk
+    | FCast(t,_,_) -> knh info t stk
+
+    | FProj (p,c) ->
+        (* if red_set info.i_flags (fCONST p) then *)
+          (match try Some (lookup_projection p (info.i_env)) with Not_found -> None with
+	  | None -> (m, stk)
+	  | Some pb ->
+	     knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
+			 :: zupdate m stk))
+	(* else (m,stk) *)
+
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
        FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) ->
         (m, stk)
 
 (* The same for pure terms *)
-and knht e t stk =
+and knht info e t stk =
   match t with
     | App(a,b) ->
-        knht e a (append_stack (mk_clos_vect e b) stk)
+        knht info e a (append_stack (mk_clos_vect e b) stk)
     | Case(ci,p,t,br) ->
-        knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
-    | Fix _ -> knh (mk_clos2 e t) stk
-    | Cast(a,_,_) -> knht e a stk
-    | Rel n -> knh (clos_rel e n) stk
+        knht info e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
+    | Fix _ -> knh info (mk_clos2 e t) stk
+    | Cast(a,_,_) -> knht info  e a stk
+    | Rel n -> knh info (clos_rel e n) stk
+    | Proj (p,c) -> knh info (mk_clos2 e t) stk
     | (Lambda _|Prod _|Construct _|CoFix _|Ind _|
        LetIn _|Const _|Var _|Evar _|Meta _|Sort _) ->
         (mk_clos2 e t, stk)
@@ -762,7 +844,7 @@ let rec knr info m stk =
       (match get_args n tys f e stk with
           Inl e', s -> knit info e' f s
         | Inr lam, s -> (lam,s))
-  | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) ->
+  | FFlex(ConstKey kn) when red_set info.i_flags (fCONST (fst kn)) ->
       (match ref_value_cache info (ConstKey kn) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
@@ -774,7 +856,7 @@ let rec knr info m stk =
       (match ref_value_cache info (RelKey k) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FConstruct(ind,c) when red_set info.i_flags fIOTA ->
+  | FConstruct((ind,c),u) when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
           (depth, args, Zcase(ci,_,br)::s) ->
             assert (ci.ci_npar>=0);
@@ -785,6 +867,10 @@ let rec knr info m stk =
             let stk' = par @ append_stack [|rarg|] s in
             let (fxe,fxbd) = contract_fix_vect fx.term in
             knit info fxe fxbd stk'
+	| (depth, args, Zproj (n, m, cst)::s) ->
+	    let rargs = drop_parameters depth n args in
+	    let rarg = project_nth_arg m rargs in
+	      kni info rarg s
         | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
@@ -798,10 +884,10 @@ let rec knr info m stk =
 
 (* Computes the weak head normal form of a term *)
 and kni info m stk =
-  let (hm,s) = knh m stk in
+  let (hm,s) = knh info m stk in
   knr info hm s
 and knit info e t stk =
-  let (ht,s) = knht e t stk in
+  let (ht,s) = knht info e t stk in
   knr info ht s
 
 let kh info v stk = fapp_stack(kni info v stk)
@@ -823,6 +909,9 @@ let whd_stack infos m stk =
 (* cache of constants: the body is computed only when needed. *)
 type clos_infos = fconstr infos
 
+let infos_env x = x.i_env
+let infos_flags x = x.i_flags
+
 let create_clos_infos flgs env =
   create (fun _ -> inject) flgs env
 
diff --git a/checker/closure.mli b/checker/closure.mli
index 13bc0c07e..9b152eb6a 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -66,11 +66,13 @@ val betaiotazeta       : reds
 val betadeltaiotanolet : reds
 
 (***********************************************************************)
-type table_key =
-  | ConstKey of constant
+type 'a tableKey =
+  | ConstKey of 'a
   | VarKey of Id.t
   | RelKey of int
 
+type table_key = constant puniverses tableKey
+
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
 val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
@@ -90,9 +92,10 @@ type fterm =
   | FAtom of constr (* Metas and Sorts *)
   | FCast of fconstr * cast_kind * fconstr
   | FFlex of table_key
-  | FInd of inductive
-  | FConstruct of constructor
+  | FInd of pinductive
+  | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
+  | FProj of constant * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCases of case_info * fconstr * fconstr * fconstr array
@@ -112,6 +115,7 @@ type fterm =
 type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
+  | Zproj of int * int * constant
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -121,6 +125,12 @@ and stack = stack_member list
 val append_stack : fconstr array -> stack -> stack
 val eta_expand_stack : stack -> stack
 
+val eta_expand_ind_stack : env -> lift -> pinductive -> fconstr -> stack -> 
+  (lift * (fconstr * stack)) -> lift * (fconstr * stack)
+ 
+val eta_expand_ind_stacks : env -> inductive -> fconstr -> stack -> 
+   (fconstr * stack) -> stack * stack
+
 (* To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
    a reduction function *)
@@ -135,6 +145,8 @@ val destFLambda :
 (* Global and local constant cache *)
 type clos_infos
 val create_clos_infos : reds -> env -> clos_infos
+val infos_env : clos_infos -> env
+val infos_flags : clos_infos -> reds
 
 (* Reduction function *)
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 4dd814d57..f500693ce 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -186,12 +186,12 @@ let make_con_equiv mpu mpc dir l =
   if mpu == mpc then constant_of_kn knu
   else constant_of_kn_equiv knu (make_kn mpc dir l)
 
-let subst_con0 sub con =
+let subst_con0 sub con u =
   let kn1,kn2 = user_con con,canonical_con con in
   let mp1,dir,l = repr_kn kn1 in
   let mp2,_,_ = repr_kn kn2 in
   let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
-  let dup con = con, Const con in
+  let dup con = con, Const (con, u) in
   let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
   match constant_of_delta_with_inline resolve con' with
     | Some t -> con', t
@@ -205,13 +205,21 @@ let subst_con0 sub con =
 let rec map_kn f f' c =
   let func = map_kn f f' in
     match c with
-      | Const kn -> (try snd (f' kn) with No_subst -> c)
-      | Ind (kn,i) ->
+      | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
+      | Proj (kn,t) -> 
+          let kn' = 
+	    try fst (f' kn Univ.Instance.empty)
+	    with No_subst -> kn 
+	  in
+	  let t' = func t in
+	    if kn' == kn && t' == t then c
+	    else Proj (kn', t')
+      | Ind ((kn,i),u) ->
 	  let kn' = f kn in
-	  if kn'==kn then c else Ind (kn',i)
-      | Construct ((kn,i),j) ->
+	  if kn'==kn then c else Ind ((kn',i),u)
+      | Construct (((kn,i),j),u) ->
 	  let kn' = f kn in
-	  if kn'==kn then c else Construct ((kn',i),j)
+	  if kn'==kn then c else Construct (((kn',i),j),u)
       | Case (ci,p,ct,l) ->
 	  let ci_ind =
             let (kn,i) = ci.ci_ind in
@@ -491,8 +499,35 @@ let eq_wf_paths = Rtree.equal eq_recarg
    with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
 *)
 
-let subst_arity sub s = subst_mps sub s
 
+let subst_decl_arity f g sub ar = 
+  match ar with
+  | RegularArity x -> 
+    let x' = f sub x in 
+      if x' == x then ar
+      else RegularArity x'
+  | TemplateArity x -> 
+    let x' = g sub x in 
+      if x' == x then ar
+      else TemplateArity x'
+
+let map_decl_arity f g = function
+  | RegularArity a -> RegularArity (f a)
+  | TemplateArity a -> TemplateArity (g a)
+
+
+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)
+
+let subst_template_cst_arity sub (ctx,s as arity) =
+  let ctx' = subst_rel_context sub ctx in
+    if ctx==ctx' then arity else (ctx',s)
+
+let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s
 
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 (* NB: we leave bytecode and native code fields untouched *)
@@ -501,6 +536,18 @@ let subst_const_body sub cb =
     const_body = subst_constant_def sub cb.const_body;
     const_type = subst_arity sub cb.const_type }
 
+
+let subst_regular_ind_arity sub s =
+  let uar' = subst_mps sub s.mind_user_arity in
+    if uar' == s.mind_user_arity then s 
+    else { mind_user_arity = uar'; mind_sort = s.mind_sort }
+
+let subst_template_ind_arity sub s = s
+
+(* FIXME records *)
+let subst_ind_arity =
+  subst_decl_arity subst_regular_ind_arity subst_template_ind_arity
+
 let subst_mind_packet sub mbp =
   { mind_consnames = mbp.mind_consnames;
     mind_consnrealdecls = mbp.mind_consnrealdecls;
@@ -508,7 +555,7 @@ let subst_mind_packet sub mbp =
     mind_typename = mbp.mind_typename;
     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_arity = subst_ind_arity sub mbp.mind_arity;
     mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
diff --git a/checker/environ.ml b/checker/environ.ml
index 79234e9e2..d650e194e 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -84,6 +84,9 @@ let add_constraints c env =
     { env with env_stratification =
       { s with env_universes = merge_constraints c s.env_universes } }
 
+let check_constraints cst env =
+  Univ.check_constraints cst env.env_stratification.env_universes
+
 (* Global constants *)
 
 let lookup_constant kn env =
@@ -104,20 +107,54 @@ let add_constant kn cs env =
 
 type const_evaluation_result = NoBody | Opaque
 
+(* Constant types *)
+
+let universes_and_subst_of cb u =
+  let univs = cb.const_universes in
+  let subst = Univ.make_universe_subst u univs in
+    subst, Univ.instantiate_univ_context subst univs
+
+let map_regular_arity f = function
+  | RegularArity a as ar -> 
+    let a' = f a in 
+      if a' == a then ar else RegularArity a'
+  | TemplateArity _ -> assert false
+
+(* constant_type gives the type of a constant *)
+let constant_type env (kn,u) =
+  let cb = lookup_constant kn env in
+    if cb.const_polymorphic then
+      let subst, csts = universes_and_subst_of cb u in
+	(map_regular_arity (subst_univs_constr subst) cb.const_type, csts)
+    else cb.const_type, Univ.Constraint.empty
+
 exception NotEvaluableConst of const_evaluation_result
 
-let constant_value env kn =
+let constant_value env (kn,u) =
   let cb = lookup_constant kn env in
-  match cb.const_body with
-    | Def l_body -> force_constr l_body
+    match cb.const_body with
+    | Def l_body -> 
+      let b = force_constr l_body in
+	if cb.const_polymorphic then
+	  let subst = Univ.make_universe_subst u cb.const_universes in
+	    subst_univs_constr subst b
+	else b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
-  try let _  = constant_value env cst in true
+  try let _  = constant_value env (cst, Univ.Instance.empty) in true
   with Not_found | NotEvaluableConst _ -> false
 
+let is_projection cst env = 
+  not (Option.is_empty (lookup_constant cst env).const_proj)
+
+let lookup_projection cst env =
+  match (lookup_constant cst env).const_proj with 
+  | Some pb -> pb
+  | None -> anomaly ("lookup_projection: constant is not a projection")
+
 (* Mutual Inductives *)
 let scrape_mind env kn=
   try
diff --git a/checker/environ.mli b/checker/environ.mli
index 46b390d0a..d3448b127 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -39,15 +39,20 @@ val push_rec_types : name array * constr array * 'a -> env -> env
 (* Universes *)
 val universes : env -> Univ.universes
 val add_constraints : Univ.constraints -> env -> env
+val check_constraints : Univ.constraints -> env -> bool
 
 (* Constants *)
 val lookup_constant : constant -> env -> Cic.constant_body
 val add_constant : constant -> Cic.constant_body -> env -> env
+val constant_type : env -> constant puniverses -> constant_type Univ.constrained
 type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
-val constant_value : env -> constant -> constr
+val constant_value : env -> constant puniverses -> constr
 val evaluable_constant : constant -> env -> bool
 
+val is_projection : constant -> env -> bool
+val lookup_projection : constant -> env -> projection_body
+
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 5927e1633..bfc20d7f8 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -139,12 +139,15 @@ let typecheck_arity env params inds =
   let nparamargs = rel_context_nhyps params in
   let nparamdecls = rel_context_length params in
   let check_arity arctxt = function
-      mar ->
-        let _ = infer_type env mar in
-          mar in
-    (* | Polymorphic par -> *)
-    (*     check_polymorphic_arity env params par; *)
-    (*     it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in *)
+    | RegularArity mar ->
+        let ar = mar.mind_user_arity in
+        let _ = infer_type env ar in
+        conv env (it_mkProd_or_LetIn (Sort mar.mind_sort) arctxt) ar;
+        ar
+    | TemplateArity par ->
+      check_polymorphic_arity env params par;
+      it_mkProd_or_LetIn (Sort(Type par.template_level)) arctxt 
+  in
   let env_arities =
     Array.fold_left
       (fun env_ar ind ->
@@ -189,8 +192,8 @@ let check_predicativity env s small level =
 
 
 let sort_of_ind = function
-    mar -> snd (destArity mar)
-  (* | Polymorphic par -> Type par.poly_level *)
+  | RegularArity mar -> mar.mind_sort
+  | TemplateArity par -> Type par.template_level
 
 let all_sorts = [InProp;InSet;InType]
 let small_sorts = [InProp;InSet]
@@ -371,12 +374,12 @@ let abstract_mind_lc env ntyps npars lc =
 let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
  (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
 
-let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
+let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
   let auxntyp = 1 in
   let specif = lookup_mind_specif env mi in
   let env' =
     push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive env specif) lpar) env in
+              hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in
   let ra_env' =
     (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
@@ -429,7 +432,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
 	    else failwith_non_pos_list n ntypes (x::largs)
 
   (* accesses to the environment are not factorised, but is it worth it? *)
-  and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) =
+  and check_positive_imbr (env,n,ntypes,ra_env as ienv) ((mi,u), largs) =
     let (mib,mip) = lookup_mind_specif env mi in
     let auxnpar = mib.mind_nparams_rec in
     let nonrecpar = mib.mind_nparams - auxnpar in
@@ -447,7 +450,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
 	let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
 	  (* Extends the environment with a variable corresponding to
 	     the inductive def *)
-	let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in
+	let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in
 	  (* Parameters expressed in env' *)
 	let lpar' = List.map (lift auxntyp) lpar in
 	let irecargs =
@@ -528,7 +531,7 @@ let check_positivity env_ar mind params nrecp inds =
 let check_inductive env kn mib =
   Flags.if_verbose ppnl (str "  checking ind: " ++ pr_mind kn); pp_flush ();
   (* check mind_constraints: should be consistent with env *)
-  let env = add_constraints mib.mind_constraints env in
+  let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index b32379b35..55acd9f97 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -39,32 +39,58 @@ let find_rectype env c =
 let find_inductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match t with
-    | Ind ind
+    | Ind (ind,_)
         when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match t with
-    | Ind ind
+    | Ind (ind,_)
         when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
     | _ -> raise Not_found
 
 let inductive_params (mib,_) = mib.mind_nparams
 
+(** Polymorphic inductives *)
+
+let make_inductive_subst mib u =
+  if mib.mind_polymorphic then 
+    make_universe_subst u mib.mind_universes
+  else Univ.empty_subst
+
+let inductive_params_ctxt (mib,u) = 
+  let subst = make_inductive_subst mib u in
+    subst_univs_context subst mib.mind_params_ctxt
+
+let inductive_instance mib =
+  if mib.mind_polymorphic then 
+    UContext.instance mib.mind_universes
+  else Instance.empty
+
+let inductive_context mib =
+  if mib.mind_polymorphic then 
+    mib.mind_universes 
+  else UContext.empty
+
+let instantiate_inductive_constraints mib subst =
+  if mib.mind_polymorphic then
+    instantiate_univ_context subst mib.mind_universes
+  else Constraint.empty
+
 (************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)
 (* inductives *)
-let ind_subst mind mib =
+let ind_subst mind mib u =
   let ntypes = mib.mind_ntypes in
-  let make_Ik k = Ind (mind,ntypes-k-1) in
+  let make_Ik k = Ind ((mind,ntypes-k-1),u) in
   List.init ntypes make_Ik
 
 (* Instantiate inductives in constructor type *)
-let constructor_instantiate mind mib c =
-  let s = ind_subst mind mib in
-  substl s c
+let constructor_instantiate mind u subst mib c =
+  let s = ind_subst mind mib u in
+  substl s (subst_univs_constr subst c)
 
 let instantiate_params full t args sign =
   let fail () =
@@ -83,13 +109,16 @@ let instantiate_params full t args sign =
   if rem_args <> [] then fail();
   substl subs ty
 
-let full_inductive_instantiate mib params sign =
+let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
   let t = mkArity (sign,dummy) in
-  fst (destArity (instantiate_params true t params mib.mind_params_ctxt))
+  let subst = make_inductive_subst mib u in
+  let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
+    subst_univs_context subst ar
 
-let full_constructor_instantiate ((mind,_),(mib,_),params) =
-  let inst_ind = constructor_instantiate mind mib in
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
+  let subst = make_inductive_subst mib u in
+  let inst_ind = constructor_instantiate mind u subst mib in
   (fun t ->
     instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
 
@@ -173,25 +202,82 @@ let rec make_subst env = function
   | [], _, _ ->
       assert false
 
-(* let instantiate_universes env ctx ar argsorts = *)
-(*   let args = Array.to_list argsorts in *)
-(*   let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in *)
-(*   let level = subst_large_constraints subst ar.poly_level in *)
-(*   ctx, *)
-(*   if is_type0m_univ level then Prop Null *)
-(*   else if is_type0_univ level then Prop Pos *)
-(*   else Type level *)
-
-let type_of_inductive_knowing_parameters env mip paramtyps =
-  mip.mind_arity
-  (* | Polymorphic ar -> *)
-  (*     let ctx = List.rev mip.mind_arity_ctxt in *)
-  (*     let ctx,s = instantiate_universes env ctx ar paramtyps in *)
-  (*     mkArity (List.rev ctx,s) *)
+
+exception SingletonInductiveBecomesProp of Id.t
+
+let instantiate_universes env ctx ar argsorts =
+  let args = Array.to_list argsorts in
+  let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+  let level = subst_large_constraints subst ar.template_level in
+  let ty =
+    (* Singleton type not containing types are interpretable in Prop *)
+    if is_type0m_univ level then Prop Null
+    (* Non singleton type not containing types are interpretable in Set *)
+    else if is_type0_univ level then Prop Pos
+    (* This is a Type with constraints *)
+    else Type level
+  in
+    (ctx, ty)
+
+(* Type of an inductive type *)
+
+let is_prop_sort = function
+  | Prop Null -> true
+  | _ -> false
+
+let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps =
+  match mip.mind_arity with
+  | RegularArity a ->
+    if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty)
+    else 
+      let subst = make_inductive_subst mib u in
+	(subst_univs_constr subst a.mind_user_arity, subst)
+  | TemplateArity ar ->
+    let ctx = List.rev mip.mind_arity_ctxt in
+    let ctx,s = instantiate_universes env ctx ar paramtyps in
+      (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
+         the situation where a non-Prop singleton inductive becomes Prop
+         when applied to Prop params *)
+      if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+      then raise (SingletonInductiveBecomesProp mip.mind_typename);
+      mkArity (List.rev ctx,s), Univ.LMap.empty
+
+let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+  match mip.mind_arity with
+  | RegularArity a ->
+    if not mib.mind_polymorphic then a.mind_user_arity
+    else 
+      let subst = make_inductive_subst mib u in
+	(subst_univs_constr subst a.mind_user_arity)
+  | TemplateArity ar ->
+    let ctx = List.rev mip.mind_arity_ctxt in
+    let ctx,s = instantiate_universes env ctx ar paramtyps in
+      (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
+         the situation where a non-Prop singleton inductive becomes Prop
+         when applied to Prop params *)
+      if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+      then raise (SingletonInductiveBecomesProp mip.mind_typename);
+      mkArity (List.rev ctx,s)
+
+let type_of_inductive env pind = 
+  type_of_inductive_gen env pind [||]
+
+let constrained_type_of_inductive env ((mib,mip),u as pind) =
+  let ty, subst = type_of_inductive_subst env pind [||] in
+  let cst = instantiate_inductive_constraints mib subst in
+    (ty, cst)
+
+let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
+  let ty, subst = type_of_inductive_subst env pind args in
+  let cst = instantiate_inductive_constraints mib subst in
+    (ty, cst)
+
+let type_of_inductive_knowing_parameters env mip args = 
+  type_of_inductive_gen env mip args
 
 (* Type of a (non applied) inductive type *)
 
-let type_of_inductive env (_,mip) =
+let type_of_inductive env mip =
   type_of_inductive_knowing_parameters env mip [||]
 
 (* The max of an array of universes *)
@@ -207,17 +293,36 @@ let max_inductive_sort =
 (************************************************************************)
 (* Type of a constructor *)
 
-let type_of_constructor cstr (mib,mip) =
+let type_of_constructor_subst cstr u subst (mib,mip) =
   let ind = inductive_of_constructor cstr in
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
-  if i > nconstr then error "Not enough constructors in the type";
-  constructor_instantiate (fst ind) mib specif.(i-1)
+  if i > nconstr then error "Not enough constructors in the type.";
+  let c = constructor_instantiate (fst ind) u subst mib specif.(i-1) in
+    c
+
+let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
+  let subst = make_inductive_subst mib u in
+    type_of_constructor_subst cstr u subst mspec, subst
+
+let type_of_constructor cstru mspec = 
+  fst (type_of_constructor_gen cstru mspec)
 
-let arities_of_specif kn (mib,mip) =
+let type_of_constructor_in_ctx cstr (mib,mip as mspec) =
+  let u = UContext.instance mib.mind_universes in
+  let c = type_of_constructor_gen (cstr, u) mspec in
+    (fst c, mib.mind_universes)
+
+let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
+  let ty, subst = type_of_constructor_gen cstru ind in
+  let cst = instantiate_inductive_constraints mib subst in
+    (ty, cst)
+
+let arities_of_specif (kn,u) (mib,mip) =
   let specif = mip.mind_nf_lc in
-  Array.map (constructor_instantiate kn mib) specif
+  let subst = make_inductive_subst mib u in
+  Array.map (constructor_instantiate kn u subst mib) specif
 
 
 
@@ -234,14 +339,16 @@ let error_elim_expln kp ki =
 (* Get type of inductive, with parameters instantiated *)
 
 let inductive_sort_family mip =
-  family_of_sort (snd (destArity mip.mind_arity))
+  match mip.mind_arity with
+  | RegularArity s -> family_of_sort s.mind_sort
+  | TemplateArity _ -> InType
 
 let mind_arity mip =
   mip.mind_arity_ctxt, inductive_sort_family mip
 
-let get_instantiated_arity (mib,mip) params =
+let get_instantiated_arity (ind,u) (mib,mip) params =
   let sign, s = mind_arity mip in
-  full_inductive_instantiate mib params sign, s
+  full_inductive_instantiate mib u params sign, s
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
@@ -269,7 +376,7 @@ let check_allowed_sort ksort specif =
     raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
 
 let is_correct_arity env c (p,pj) ind specif params =
-  let arsign,_ = get_instantiated_arity specif params in
+  let arsign,_ = get_instantiated_arity ind specif params in
   let rec srec env pt ar =
     let pt' = whd_betadeltaiota env pt in
     match pt', ar with
@@ -305,9 +412,9 @@ let is_correct_arity env c (p,pj) ind specif 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 (_,mip as specif) params dep p =
+let build_branches_type (ind,u) (_,mip as specif) params dep p =
   let build_one_branch i cty =
-    let typi = full_constructor_instantiate (ind,specif,params) cty in
+    let typi = full_constructor_instantiate (ind,u,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
@@ -316,7 +423,7 @@ let build_branches_type ind (_,mip as specif) params dep p =
       if dep then
         let cstr = ith_constructor_of_inductive ind (i+1) in
         let dep_cstr =
-          applist (Construct cstr,lparams@extended_rel_list 0 args) in
+          applist (Construct (cstr,u),lparams@extended_rel_list 0 args) in
         vargs @ [dep_cstr]
       else
         vargs in
@@ -330,12 +437,12 @@ let build_case_type dep p c realargs =
   let args = if dep then realargs@[c] else realargs in
   beta_appvect p (Array.of_list args)
 
-let type_case_branches env (ind,largs) (p,pj) c =
-  let specif = lookup_mind_specif env ind in
+let type_case_branches env (pind,largs) (p,pj) c =
+  let specif = lookup_mind_specif env (fst pind) in
   let nparams = inductive_params specif in
   let (params,realargs) = List.chop nparams largs in
-  let dep = is_correct_arity env c (p,pj) ind specif params in
-  let lc = build_branches_type ind specif params dep p in
+  let dep = is_correct_arity env c (p,pj) pind specif params in
+  let lc = build_branches_type pind specif params dep p in
   let ty = build_case_type dep p c realargs in
   (lc, ty)
 
@@ -724,11 +831,11 @@ let check_one_fix renv recpos def =
                    else check_rec_call renv' [] body)
                 bodies
 
-        | Const kn ->
+        | Const (kn,u) ->
             if evaluable_constant kn renv.env then
               try List.iter (check_rec_call renv []) l
               with (FixGuardError _ ) ->
-		let value = (applist(constant_value renv.env kn, l)) in
+		let value = (applist(constant_value renv.env (kn,u), l)) in
 	        check_rec_call renv stack value
 	    else List.iter (check_rec_call renv []) l
 
@@ -761,6 +868,8 @@ let check_one_fix renv recpos def =
 
         | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
+	| Proj (p, c) -> check_rec_call renv [] c
+
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
@@ -859,7 +968,7 @@ let check_one_cofix env nbfix def deftype =
             else if not(List.for_all (noccur_with_meta n nbfix) args) then
 	      raise (CoFixGuardError (env,NestedRecursiveOccurrences))
 
-	| Construct (_,i as cstr_kn)  ->
+	| Construct ((_,i as cstr_kn),u)  ->
             let lra = vlra.(i-1) in
             let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 082bdae19..e223af0c9 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -14,7 +14,7 @@ open Environ
 
 (*s Extracting an inductive type from a construction *)
 
-val find_rectype : env -> constr -> inductive * constr list
+val find_rectype : env -> constr -> pinductive * constr list
 
 type mind_specif = mutual_inductive_body * one_inductive_body
 
@@ -22,12 +22,15 @@ type mind_specif = mutual_inductive_body * one_inductive_body
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
-val type_of_inductive : env -> mind_specif -> constr
+val make_inductive_subst : mutual_inductive_body -> Univ.universe_instance -> Univ.universe_subst
+val inductive_instance : mutual_inductive_body -> Univ.universe_instance
+
+val type_of_inductive : env -> mind_specif puniverses -> constr
 
 (* Return type as quoted by the user *)
-val type_of_constructor : constructor -> mind_specif -> constr
+val type_of_constructor : pconstructor -> mind_specif -> constr
 
-val arities_of_specif : mutual_inductive -> mind_specif -> constr array
+val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array
 
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
@@ -36,7 +39,7 @@ val arities_of_specif : mutual_inductive -> mind_specif -> constr array
    introduced by products) and the type for the whole expression.
  *)
 val type_case_branches :
-  env -> inductive * constr list -> constr * constr -> constr
+  env -> pinductive * constr list -> constr * constr -> constr
     -> constr array * constr
 
 (* Check a [case_info] actually correspond to a Case expression on the
@@ -50,12 +53,12 @@ val check_cofix : env -> cofixpoint -> unit
 (*s Support for sort-polymorphic inductive types *)
 
 val type_of_inductive_knowing_parameters :
-  env -> one_inductive_body -> constr array -> constr
+  env -> mind_specif puniverses -> constr array -> constr
 
 val max_inductive_sort : sorts array -> Univ.universe
 
-(* val instantiate_universes : env -> rel_context -> *)
-(*     inductive_arity -> constr array -> rel_context * sorts *)
+val instantiate_universes : env -> rel_context ->
+  template_arity -> constr array -> rel_context * sorts
 
 (***************************************************************)
 (* Debug *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 53316a2cb..12a97bf68 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -14,30 +14,31 @@ open Environ
 
 (** {6 Checking constants } *)
 
-(* let refresh_arity ar = *)
-(*   let ctxt, hd = decompose_prod_assum ar in *)
-(*   match hd with *)
-(*       Sort (Type u) when not (Univ.is_univ_variable u) -> *)
-(*         let u' = Univ.fresh_local_univ() in *)
-(*         mkArity (ctxt,Type u'), *)
-(*         Univ.enforce_leq u u' Univ.empty_constraint *)
-(*     | _ -> ar, Univ.empty_constraint *)
+let refresh_arity ar =
+  let ctxt, hd = decompose_prod_assum ar in
+  match hd with
+      Sort (Type u) when not (Univ.is_univ_variable u) ->
+        let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in
+        mkArity (ctxt,Prop Null), 
+	  Univ.enforce_leq u u' Univ.empty_constraint
+    | _ -> ar, Univ.empty_constraint
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn);
-(*  let env = add_constraints cb.const_constraints env in*)
+  let env = add_constraints (Univ.UContext.constraints cb.const_universes) env in
   (match cb.const_type with
-      ty ->
-        let env' = add_constraints cb.const_constraints env in (*MS: FIXME*)
-	let _ = infer_type env' ty in
-          (match body_of_constant cb with
+      RegularArity ty ->
+        let ty, cu = refresh_arity ty in
+        let envty = add_constraints cu env in
+        let _ = infer_type envty ty in
+        (match body_of_constant cb with
           | Some bd ->
-              let j = infer env' bd in
-              conv_leq env' j ty
+              let j = infer envty bd in
+              conv_leq envty j ty
           | None -> ())
-    (* | PolymorphicArity(ctxt,par) -> *)
-    (*     let _ = check_ctxt env ctxt in *)
-    (*     check_polymorphic_arity env ctxt par *));
+    | TemplateArity(ctxt,par) ->
+        let _ = check_ctxt env ctxt in
+        check_polymorphic_arity env ctxt par);
   add_constant kn cb env
 
 
diff --git a/checker/modops.ml b/checker/modops.ml
index 2d20dd0f3..c27c5d598 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -90,7 +90,11 @@ let strengthen_const mp_from l cb resolver =
     | _ ->
       let con = Constant.make2 mp_from l in
       (* let con =  constant_of_delta resolver con in*)
-      { cb with const_body = Def (Declarations.from_val (Const con)) }
+      let u = 
+	if cb.const_polymorphic then Univ.UContext.instance cb.const_universes 
+	else Univ.Instance.empty
+      in
+      { cb with const_body = Def (Declarations.from_val (Const (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
diff --git a/checker/print.ml b/checker/print.ml
index f25b8cf09..8a5464dae 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -10,6 +10,8 @@ open Format
 open Cic
 open Names
 
+let print_instance i = Pp.pp (Univ.Instance.pr i)
+
 let print_pure_constr csr =
   let rec term_display c = match  c with
   | Rel n -> print_string "#"; print_int n
@@ -43,19 +45,22 @@ let print_pure_constr csr =
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string ")"
   | Evar _ -> print_string "Evar#"
-  | Const c -> print_string "Cons(";
+  | Const (c,u) -> print_string "Cons(";
       sp_con_display c;
+      print_string ","; print_instance u;
       print_string ")"
-  | Ind (sp,i) ->
+  | Ind ((sp,i),u) ->
       print_string "Ind(";
       sp_display sp;
       print_string ","; print_int i;
+      print_string ","; print_instance u;
       print_string ")"
-  | Construct ((sp,i),j) ->
+  | Construct (((sp,i),j),u) ->
       print_string "Constr(";
       sp_display sp;
       print_string ",";
-      print_int i; print_string ","; print_int j; print_string ")"
+      print_int i; print_string ","; print_int j; 
+      print_string ","; print_instance u; print_string ")"
   | Case (ci,p,c,bl) ->
       open_vbox 0;
       print_string "<"; box_display p; print_string ">";
@@ -94,6 +99,9 @@ let print_pure_constr csr =
 	  print_cut();
         done
       in print_string"{"; print_fix (); print_string"}"
+  | Proj (p, c) ->
+    print_string "Proj("; sp_con_display p; print_string ","; 
+    box_display c; print_string ")"
 
   and box_display c = open_hovbox 1; term_display c; close_box()
 
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 54d79484e..384b9ad7f 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -50,6 +50,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
+  | Zlproj of Names.constant * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -68,6 +69,8 @@ let pure_stack lfts stk =
             | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
             | (Zapp a, (l,pstk)) ->
                 (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
+	    | (Zproj (n,m,c), (l,pstk)) ->
+		(l, Zlproj (c,l)::pstk)
             | (Zfix(fx,a),(l,pstk)) ->
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
@@ -116,6 +119,10 @@ type 'a conversion_function = env -> 'a -> 'a -> unit
 exception NotConvertible
 exception NotConvertibleVect of int
 
+let convert_universes univ u u' =
+  if Univ.Instance.check_eq univ u u' then ()
+  else raise NotConvertible
+
 let compare_stacks f fmind lft1 stk1 lft2 stk2 =
   let rec cmp_rec pstk1 pstk2 =
     match (pstk1,pstk2) with
@@ -163,6 +170,7 @@ let rec no_arg_available = function
   | Zupdate _ :: stk -> no_arg_available stk
   | Zshift _ :: stk -> no_arg_available stk
   | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
+  | Zproj _ :: _ -> true
   | Zcase _ :: _ -> true
   | Zfix _ :: _ -> true
 
@@ -174,6 +182,7 @@ let rec no_nth_arg_available n = function
       let k = Array.length v in
       if n >= k then no_nth_arg_available (n-k) stk
       else false
+  | Zproj _ :: _ -> true
   | Zcase _ :: _ -> true
   | Zfix _ :: _ -> true
 
@@ -182,6 +191,7 @@ let rec no_case_available = function
   | Zupdate _ :: stk -> no_case_available stk
   | Zshift _ :: stk -> no_case_available stk
   | Zapp _ :: stk -> no_case_available stk
+  | Zproj (_,_,_) :: _ -> false
   | Zcase _ :: _ -> false
   | Zfix _ :: _ -> true
 
@@ -192,7 +202,7 @@ let in_whnf (t,stk) =
     | FConstruct _ -> no_case_available stk
     | FCoFix _ -> no_case_available stk
     | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk
-    | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true
+    | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
     | FLOCKED -> assert false
 
 let oracle_order fl1 fl2 =
@@ -201,6 +211,15 @@ let oracle_order fl1 fl2 =
     | _, ConstKey _ -> true
     | _ -> false
 
+let unfold_projection infos p c =
+  (* if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then *)
+    (match try Some (lookup_projection p (infos_env infos)) with Not_found -> None with
+    | Some pb -> 
+      let s = Zproj (pb.proj_npars, pb.proj_arg, p) in
+	Some (c, s)
+    | None -> None)
+  (* else None *)
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
   eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -255,19 +274,49 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
           let (app1,app2) =
             if oracle_order fl1 fl2 then
               match unfold_reference infos fl1 with
-                | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
-                | None ->
-                    (match unfold_reference infos fl2 with
-                      | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
-                     | None -> raise NotConvertible)
+              | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+              | None ->
+                (match unfold_reference infos fl2 with
+                | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+                | None -> raise NotConvertible)
             else
 	      match unfold_reference infos fl2 with
-                | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
-                | None ->
-                    (match unfold_reference infos fl1 with
-                    | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
-		    | None -> raise NotConvertible) in
-          eqappr univ cv_pb infos app1 app2)
+              | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+              | None ->
+                (match unfold_reference infos fl1 with
+                | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+		| None -> raise NotConvertible) in
+            eqappr univ cv_pb infos app1 app2)
+	  
+    | (FProj (p1,c1), FProj (p2, c2)) ->
+      (* Projections: prefer unfolding to first-order unification,
+	 which will happen naturally if the terms c1, c2 are not in constructor
+	 form *)
+      (match unfold_projection infos p1 c1 with
+      | Some (def1,s1) -> 
+	eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
+      | None ->
+	match unfold_projection infos p2 c2 with
+	| Some (def2,s2) ->
+	  eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
+	| None -> 
+          if Names.eq_con_chk p1 p2 && compare_stack_shape v1 v2 then
+	    let () = ccnv univ CONV infos el1 el2 c1 c2 in
+	      convert_stacks univ infos lft1 lft2 v1 v2
+	  else (* Two projections in WHNF: unfold *)
+	    raise NotConvertible)
+
+    | (FProj (p1,c1), t2) ->
+      (match unfold_projection infos p1 c1 with
+      | Some (def1,s1) ->
+         eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
+      | None -> raise NotConvertible)
+      
+    | (_, FProj (p2,c2)) ->
+      (match unfold_projection infos p2 c2 with
+      | Some (def2,s2) -> 
+         eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
+      | None -> raise NotConvertible)
 
     (* other constructors *)
     | (FLambda _, FLambda _) ->
@@ -300,29 +349,47 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
           (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
 
     (* only one constant, defined var or defined rel *)
-    | (FFlex fl1, _)      ->
+    | (FFlex fl1, c2)      ->
         (match unfold_reference infos fl1 with
            | Some def1 ->
 	       eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
-           | None -> raise NotConvertible)
-    | (_, FFlex fl2)      ->
+           | None -> 
+	     match c2 with 
+	     | FConstruct ((ind2,j2),u2) ->
+	       (try
+ 	     	  let v2, v1 = 
+ 		    eta_expand_ind_stacks (infos_env infos) ind2 hd2 v2 (snd appr1)
+ 		  in convert_stacks univ infos lft1 lft2 v1 v2
+ 	     	with Not_found -> raise NotConvertible)
+	     | _ -> raise NotConvertible)
+
+    | (c1, FFlex fl2)      ->
         (match unfold_reference infos fl2 with
            | Some def2 ->
 	       eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
-           | None -> raise NotConvertible)
+           | None -> 
+	     match c1 with 
+	     | FConstruct ((ind1,j1),u1) ->
+ 	       (try let v1, v2 = 
+		      eta_expand_ind_stacks (infos_env infos) ind1 hd1 v1 (snd appr2)
+		    in convert_stacks univ infos lft1 lft2 v1 v2
+		with Not_found -> raise NotConvertible)
+	     | _ -> raise NotConvertible)
 
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
-     | (FInd ind1, FInd ind2) ->
-         if mind_equiv_infos infos ind1 ind2
-	 then
-           convert_stacks univ infos lft1 lft2 v1 v2
-         else raise NotConvertible
+    | (FInd (ind1,u1), FInd (ind2,u2)) ->
+        if mind_equiv_infos infos ind1 ind2
+	then
+	  (let () = convert_universes univ u1 u2 in
+           convert_stacks univ infos lft1 lft2 v1 v2)
+        else raise NotConvertible
 
-     | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
+     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
 	 if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2
 	 then
-           convert_stacks univ infos lft1 lft2 v1 v2
+	  (let () = convert_universes univ u1 u2 in
+           convert_stacks univ infos lft1 lft2 v1 v2)
          else raise NotConvertible
 
      | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 070ed1924..6c66ca60b 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -93,6 +93,15 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       | _ -> error ()
   in
   let mib2 =  subst_mind subst2 mib2 in
+  let check eq f = if not (eq (f mib1) (f mib2)) then error () in
+  let bool_equal (x : bool) (y : bool) = x = y in
+  let u = 
+    check bool_equal (fun x -> x.mind_polymorphic);
+    if mib1.mind_polymorphic then (
+      check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes);
+      UContext.instance mib1.mind_universes)
+    else Instance.empty
+  in
   let check_inductive_type env t1 t2 =
 
     (* Due to sort-polymorphism in inductive types, the conclusions of
@@ -146,15 +155,13 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
       check_inductive_type env
-        (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
+        (type_of_inductive env ((mib1,p1),u)) (type_of_inductive env ((mib2,p2),u))
   in
   let check_cons_types i p1 p2 =
     Array.iter2 (check_conv conv env)
-      (arities_of_specif kn (mib1,p1))
-      (arities_of_specif kn (mib2,p2))
+      (arities_of_specif (kn,u) (mib1,p1))
+      (arities_of_specif (kn,u) (mib2,p2))
   in
-  let check eq f = if not (eq (f mib1) (f mib2)) then error () in
-  let bool_equal (x : bool) (y : bool) = x = y in
   check bool_equal (fun mib -> mib.mind_finite);
   check Int.equal (fun mib -> mib.mind_ntypes);
   assert (Array.length mib1.mind_packets >= 1
@@ -179,8 +186,15 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
 	    if kn1 <> kn2 then error ()
   end;*)
   (* we check that records and their field names are preserved. *)
-  check bool_equal (fun mib -> mib.mind_record);
-  if mib1.mind_record then begin
+  let record_equal x y =
+    match x, y with
+    | None, None -> true
+    | Some (r1,p1), Some (r2,p2) ->
+      eq_constr r1 r2 && Array.for_all2 eq_con_chk p1 p2
+    | _, _ -> false
+  in
+  check record_equal (fun mib -> mib.mind_record);
+  if mib1.mind_record != None then begin
     let rec names_prod_letin t = match t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)
@@ -282,7 +296,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		      "inductive type and give a definition to map the old name to the new " ^
 		      "name."));
       if constant_has_body cb2 then error () ;
-      let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
+      let u = inductive_instance mind1 in
+      let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
@@ -292,7 +307,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
        "constructor and give a definition to map the old name to the new " ^
        "name."));
       if constant_has_body cb2 then error () ;
-      let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
+      let u1 = inductive_instance mind1 in
+      let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv env ty1 ty2
 
diff --git a/checker/term.ml b/checker/term.ml
index ea81f5dab..ad26c5edc 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -76,6 +76,7 @@ let iter_constr_with_binders g f n c = match c with
   | CoFix (_,(_,tl,bl)) ->
       Array.iter (f n) tl;
       Array.iter (f (iterate g (Array.length tl) n)) bl
+  | Proj (p, c) -> f n c
 
 exception LocalOccur
 
@@ -152,6 +153,7 @@ let map_constr_with_binders g f l c = match c with
   | CoFix(ln,(lna,tl,bl)) ->
       let l' = iterate g (Array.length tl) l in
       CoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+  | Proj (p, c) -> Proj (p, f l c)
 
 (* The generic lifting function *)
 let rec exliftn el c = match c with
@@ -351,6 +353,9 @@ let compare_sorts s1 s2 = match s1, s2 with
 | Prop _, Type _ -> false
 | Type _, Prop _ -> false
 
+let eq_puniverses f (c1,u1) (c2,u2) =
+  Univ.Instance.equal u1 u2 && f c1 c2
+
 let compare_constr f t1 t2 =
   match t1, t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
@@ -372,9 +377,10 @@ let compare_constr f t1 t2 =
           f h1 h2 && List.for_all2 f l1 l2
         else false
   | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
-  | Const c1, Const c2 -> eq_con_chk c1 c2
-  | Ind c1, Ind c2 -> eq_ind_chk c1 c2
-  | Construct (c1,i1), Construct (c2,i2) -> Int.equal i1 i2 && eq_ind_chk c1 c2
+  | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2
+  | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2
+  | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2
+    && Univ.Instance.equal u1 u2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
       f p1 p2 && f c1 c2 && Array.equal f bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
@@ -389,3 +395,88 @@ let rec eq_constr m n =
   compare_constr eq_constr m n
 
 let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
+
+(* Universe substitutions *)
+
+let subst_univs_puniverses subst =
+  if Univ.is_empty_level_subst subst then fun c -> c
+  else 
+    let f = Univ.Instance.subst subst in
+      fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u')
+
+let subst_univs_fn_puniverses fn =
+  let f = Univ.Instance.subst_fn fn in
+    fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u')
+
+let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c
+
+let subst_univs_fn_constr f c =
+  let changed = ref false in
+  let fu = Univ.subst_univs_universe f in
+  let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in
+  let rec aux t = 
+    match t with
+    | Sort (Type u) -> 
+      let u' = fu u in
+	if u' == u then t else 
+	  (changed := true; Sort (Type u'))
+    | Const (c, u) -> 
+      let u' = fi u in 
+	if u' == u then t
+	else (changed := true; Const (c, u'))
+    | Ind (i, u) ->
+      let u' = fi u in 
+	if u' == u then t
+	else (changed := true; Ind (i, u'))
+    | Construct (c, u) ->
+      let u' = fi u in 
+	if u' == u then t
+	else (changed := true; Construct (c, u'))
+    | _ -> map_constr aux t
+  in 
+  let c' = aux c in
+    if !changed then c' else c
+
+let subst_univs_constr subst c =
+  if Univ.is_empty_subst subst then c
+  else 
+    let f = Univ.make_subst subst in
+      subst_univs_fn_constr f c
+
+
+let subst_univs_level_constr subst c =
+  if Univ.is_empty_level_subst subst then c
+  else 
+    let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in
+    let changed = ref false in
+    let rec aux t = 
+      match t with
+      | Const (c, u) -> 
+	if Univ.Instance.is_empty u then t
+	else 
+          let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; Const (c, u'))
+      | Ind (i, u) ->
+	if Univ.Instance.is_empty u then t
+	else 
+	  let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; Ind (i, u'))
+      | Construct (c, u) ->
+	if Univ.Instance.is_empty u then t
+	else 
+          let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; Construct (c, u'))
+      | Sort (Type u) -> 
+         let u' = Univ.subst_univs_level_universe subst u in
+	   if u' == u then t else 
+	     (changed := true; Sort (Type u'))
+      | _ -> map_constr aux t
+    in
+    let c' = aux c in
+      if !changed then c' else c
+
+let subst_univs_context s = 
+  map_rel_context (subst_univs_constr s)
diff --git a/checker/term.mli b/checker/term.mli
index f75341b9d..cf488f536 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -52,3 +52,7 @@ val destArity : constr -> arity
 val isArity : constr -> bool
 val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 val eq_constr : constr -> constr -> bool
+
+val subst_univs_constr : Univ.universe_subst -> constr -> constr
+val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
+val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index e800ee3ef..565005b90 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -45,7 +45,7 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
-  | ElimArity of inductive * sorts_family list * constr * unsafe_judgment
+  | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of unsafe_judgment
   | WrongCaseInfo of inductive * case_info
@@ -59,6 +59,7 @@ type type_error =
   | IllFormedRecBody of guard_error * name array * int
   | IllTypedRecBody of
       int * name array * unsafe_judgment array * constr array
+  | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error
 
@@ -107,4 +108,5 @@ let error_ill_formed_rec_body env why lna i =
 let error_ill_typed_rec_body env i lna vdefj vargs =
   raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
-
+let error_unsatisfied_constraints env c =
+  raise (TypeError (env, UnsatisfiedConstraints c))
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index bcd4360b3..24086f16f 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -47,7 +47,7 @@ type type_error =
   | NotAType of unsafe_judgment
   | BadAssumption of unsafe_judgment
   | ReferenceVariables of constr
-  | ElimArity of inductive * sorts_family list * constr * unsafe_judgment
+  | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of unsafe_judgment
   | WrongCaseInfo of inductive * case_info
@@ -61,6 +61,7 @@ type type_error =
   | IllFormedRecBody of guard_error * name array * int
   | IllTypedRecBody of
       int * name array * unsafe_judgment array * constr array
+  | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error
 
@@ -75,7 +76,7 @@ val error_assumption : env -> unsafe_judgment -> 'a
 val error_reference_variables : env -> constr -> 'a
 
 val error_elim_arity :
-  env -> inductive -> sorts_family list -> constr -> unsafe_judgment ->
+  env -> pinductive -> sorts_family list -> constr -> unsafe_judgment ->
       (sorts_family * sorts_family * arity_error) option -> 'a
 
 val error_case_not_inductive : env -> unsafe_judgment -> 'a
@@ -99,3 +100,4 @@ val error_ill_formed_rec_body :
 val error_ill_typed_rec_body  :
   env -> int -> name array -> unsafe_judgment array -> constr array -> 'a
 
+val error_unsatisfied_constraints : env -> Univ.constraints -> 'a
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 6a705b198..887d9dc1d 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -28,6 +28,10 @@ let conv_leq_vecti env v1 v2 =
     v1
     v2
 
+let check_constraints cst env = 
+  if Environ.check_constraints cst env then ()
+  else error_unsatisfied_constraints env cst
+
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env (c,ty as j) =
   match whd_betadeltaiota env ty with
@@ -66,23 +70,34 @@ let judge_of_relative env n =
 
 (* Type of constants *)
 
-let type_of_constant_knowing_parameters env t paramtyps =
-  t
-  (* | PolymorphicArity (sign,ar) -> *)
-  (*     let ctx = List.rev sign in *)
-  (*     let ctx,s = instantiate_universes env ctx ar paramtyps in *)
-  (*     mkArity (List.rev ctx,s) *)
+
+let type_of_constant_type_knowing_parameters env t paramtyps =
+  match t with
+  | RegularArity t -> t
+  | TemplateArity (sign,ar) ->
+      let ctx = List.rev sign in
+      let ctx,s = instantiate_universes env ctx ar paramtyps in
+      mkArity (List.rev ctx,s)
+
+let type_of_constant_knowing_parameters env cst paramtyps =
+  let ty, cu = constant_type env cst in
+    type_of_constant_type_knowing_parameters env ty paramtyps, cu
 
 let type_of_constant_type env t =
-  type_of_constant_knowing_parameters env t [||]
+  type_of_constant_type_knowing_parameters env t [||]
 
-let judge_of_constant_knowing_parameters env cst paramstyp =
-  let cb =
-    try lookup_constant cst env
+let type_of_constant env cst =
+  type_of_constant_knowing_parameters env cst [||]
+
+let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
+  let _cb =
+    try lookup_constant kn env
     with Not_found ->
-      failwith ("Cannot find constant: "^string_of_con cst)
+      failwith ("Cannot find constant: "^string_of_con kn)
   in
-  type_of_constant_knowing_parameters env cb.const_type paramstyp
+  let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
+  let () = check_constraints cu env in
+    ty
 
 let judge_of_constant env cst =
   judge_of_constant_knowing_parameters env cst [||]
@@ -160,27 +175,27 @@ let judge_of_cast env (c,cj) k tj =
    the App case of execute; from this constraints, the expected
    dynamic constraints of the form u<=v are enforced *)
 
-let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
-  let (mib,mip) =
+let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
+  let specif =
     try lookup_mind_specif env ind
     with Not_found ->
       failwith ("Cannot find inductive: "^string_of_mind (fst ind))
   in
-  type_of_inductive_knowing_parameters env mip paramstyp
+  type_of_inductive_knowing_parameters env (specif,u) paramstyp
 
 let judge_of_inductive env ind =
   judge_of_inductive_knowing_parameters env ind [||]
 
 (* Constructors. *)
 
-let judge_of_constructor env c =
+let judge_of_constructor env (c,u) =
   let ind = inductive_of_constructor c in
   let specif =
     try lookup_mind_specif env ind
     with Not_found ->
       failwith ("Cannot find inductive: "^string_of_mind (fst ind))
   in
-  type_of_constructor c specif
+  type_of_constructor (c,u) specif
 
 (* Case. *)
 
@@ -196,11 +211,24 @@ let judge_of_case env ci pj (c,cj) lfj =
   let indspec =
     try find_rectype env cj
     with Not_found -> error_case_not_inductive env (c,cj) in
-  let _ = check_case_info env (fst indspec) ci in
+  let _ = check_case_info env (fst (fst indspec)) ci in
   let (bty,rslty) = type_case_branches env indspec pj c in
   check_branch_types env (c,cj) (lfj,bty);
   rslty
 
+(* Projection. *)
+
+let judge_of_projection env p c ct =
+  let pb = lookup_projection p env in
+  let (ind,u), args =
+    try find_rectype env ct
+    with Not_found -> error_case_not_inductive env (c, ct)
+  in
+    assert(eq_mind pb.proj_ind (fst ind));
+    let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
+    let ty = subst_univs_constr usubst pb.proj_type in
+      substl (c :: List.rev args) ty
+
 (* Fixpoints. *)
 
 (* Checks the type of a general (co)fixpoint, i.e. without checking *)
@@ -264,6 +292,10 @@ let rec execute env cstr =
         let jl = Array.map2 (fun c ty -> c,ty) args jl in
 	judge_of_apply env (f,j) jl
 
+    | Proj (p, c) ->
+        let ct = execute env c in
+          judge_of_projection env p c ct
+
     | Lambda (name,c1,c2) ->
         let _ = execute_type env c1 in
 	let env1 = push_rel (name,None,c1) env in
@@ -364,14 +396,14 @@ let check_kind env ar u =
   if snd (dest_prod env ar) = Sort(Type u) then ()
   else failwith "not the correct sort"
 
-(* let check_polymorphic_arity env params par = *)
-(*   let pl = par.poly_param_levels in *)
-(*   let rec check_p env pl params = *)
-(*     match pl, params with *)
-(*         Some u::pl, (na,None,ty)::params -> *)
-(*           check_kind env ty u; *)
-(*           check_p (push_rel (na,None,ty) env) pl params *)
-(*       | None::pl,d::params -> check_p (push_rel d env) pl params *)
-(*       | [], _ -> () *)
-(*       | _ -> failwith "check_poly: not the right number of params" in *)
-(*   check_p env pl (List.rev params) *)
+let check_polymorphic_arity env params par =
+  let pl = par.template_param_levels in
+  let rec check_p env pl params =
+    match pl, params with
+        Some u::pl, (na,None,ty)::params ->
+          check_kind env ty u;
+          check_p (push_rel (na,None,ty) env) pl params
+      | None::pl,d::params -> check_p (push_rel d env) pl params
+      | [], _ -> ()
+      | _ -> failwith "check_poly: not the right number of params" in
+  check_p env pl (List.rev params)
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 97d79fe54..32920b02f 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -16,8 +16,8 @@ open Environ
 val infer      : env -> constr      -> constr
 val infer_type : env -> constr      -> sorts
 val check_ctxt : env -> rel_context -> env
-(* val check_polymorphic_arity : *)
-(*   env -> rel_context -> polymorphic_arity -> unit *)
+val check_polymorphic_arity :
+  env -> rel_context -> template_arity -> unit
 
-val type_of_constant_type : env -> constr -> constr
+val type_of_constant_type : env -> constant_type -> constr