Imported Upstream version 8.5~beta1+dfsg

1 files changed, 383 insertions, 227 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 20aaf52a..99d9f52c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -1,22 +1,34 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
 open Term
+open Vars
+open Context
 open Declarations
+open Declareops
 open Inductive
-open Sign
 open Environ
 open Reduction
 open Typeops
 open Entries
+open Pp
+
+(* Tell if indices (aka real arguments) contribute to size of inductive type *)
+(* If yes, this is compatible with the univalent model *)
+
+let indices_matter = ref false
+
+let enforce_indices_matter () = indices_matter := true
+let is_indices_matter () = !indices_matter
 
 (* Same as noccur_between but may perform reductions.
    Could be refined more...  *)
@@ -37,11 +49,11 @@ let is_constructor_head t =
 type inductive_error =
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
-  | NotConstructor of env * identifier * constr * constr * int * int
+  | NotConstructor of env * Id.t * constr * constr * int * int
   | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of identifier
-  | SameNamesConstructors of identifier
-  | SameNamesOverlap of identifier list
+  | SameNamesTypes of Id.t
+  | SameNamesConstructors of Id.t
+  | SameNamesOverlap of Id.t list
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
@@ -57,10 +69,10 @@ let check_constructors_names =
   let rec check idset = function
     | [] -> idset
     | c::cl ->
-	if Idset.mem c idset then
+	if Id.Set.mem c idset then
 	  raise (InductiveError (SameNamesConstructors c))
 	else
-	  check (Idset.add c idset) cl
+	  check (Id.Set.add c idset) cl
   in
   check
 
@@ -74,13 +86,13 @@ let mind_check_names mie =
     | ind::inds ->
 	let id = ind.mind_entry_typename in
 	let cl = ind.mind_entry_consnames in
-	if Idset.mem id indset then
+	if Id.Set.mem id indset then
 	  raise (InductiveError (SameNamesTypes id))
 	else
 	  let cstset' = check_constructors_names cstset cl in
-	  check (Idset.add id indset) cstset' inds
+	  check (Id.Set.add id indset) cstset' inds
   in
-  check Idset.empty Idset.empty mie.mind_entry_inds
+  check Id.Set.empty Id.Set.empty mie.mind_entry_inds
 (* The above verification is not necessary from the kernel point of
   vue since inductive and constructors are not referred to by their
   name, but only by the name of the inductive packet and an index. *)
@@ -90,40 +102,28 @@ let mind_check_names mie =
 
 (* Typing the arities and constructor types *)
 
-let is_logic_type t = (t.utj_type = prop_sort)
-
-(* [infos] is a sequence of pair [islogic,issmall] for each type in
-   the product of a constructor or arity *)
-
-let is_small infos = List.for_all (fun (logic,small) -> small) infos
-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, conjunction of logical properties
 *)
 let is_unit constrsinfos =
   match constrsinfos with  (* One info = One constructor *)
-   | [constrinfos] -> is_logic_constr constrinfos
+   | [level] -> is_type0m_univ level
    | [] -> (* type without constructors *) true
    | _ -> false
 
-let rec infos_and_sort env t =
-  let t = whd_betadeltaiota env t in
-  match kind_of_term t with
-    | Prod (name,c1,c2) ->
-        let (varj,_) = infer_type env c1 in
+let infos_and_sort env ctx t =
+  let rec aux env ctx t max =
+    let t = whd_betadeltaiota env t in
+      match kind_of_term t with
+      | Prod (name,c1,c2) ->
+        let varj = infer_type env c1 in
 	let env1 = Environ.push_rel (name,None,varj.utj_val) env in
-	let logic = is_logic_type varj in
-	let small = Term.is_small varj.utj_type in
-	(logic,small) :: (infos_and_sort env1 c2)
-    | _ when is_constructor_head t -> []
-    | _ -> (* don't fail if not positive, it is tested later *) []
-
-let small_unit constrsinfos =
-  let issmall = List.for_all is_small constrsinfos
-  and isunit = is_unit constrsinfos in
-  issmall, isunit
+	let max = Universe.sup max (univ_of_sort varj.utj_type) in
+	  aux env1 ctx c2 max
+    | _ when is_constructor_head t -> max
+    | _ -> (* don't fail if not positive, it is tested later *) max
+  in aux env ctx t Universe.type0m
 
 (* Computing the levels of polymorphic inductive types
 
@@ -145,140 +145,206 @@ let small_unit constrsinfos =
    w1,w2,w3 <= u3
 *)
 
-let extract_level (_,_,_,lc,lev) =
-  (* Enforce that the level is not in Prop if more than two constructors *)
-  if Array.length lc >= 2 then sup type0_univ lev else lev
-
-let inductive_levels arities inds =
-  let levels = Array.map pi3 arities in
-  let cstrs_levels = Array.map extract_level inds in
-  (* Take the transitive closure of the system of constructors *)
-  (* level constraints and remove the recursive dependencies *)
-  solve_constraints_system levels cstrs_levels
-
 (* This (re)computes informations relevant to extraction and the sort of an
    arity or type constructor; we do not to recompute universes constraints *)
 
-let constraint_list_union =
-  List.fold_left union_constraints empty_constraint
-
-let infer_constructor_packet env_ar_par params lc =
+let infer_constructor_packet env_ar_par ctx params lc =
   (* 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 = List.map (infer_type env_ar_par) lc 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)
+  (* compute the max of the sorts of the products of the constructors types *)
+  let levels = List.map (infos_and_sort env_ar_par ctx) lc in
+  let isunit = is_unit levels in
+  let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in
+  let level = List.fold_left (fun max l -> Universe.sup max l) min levels in
+  (lc'', (isunit, level))
+
+(* If indices matter *)
+let cumulate_arity_large_levels env sign =
+  fst (List.fold_right
+    (fun (_,_,t as d) (lev,env) ->
+      let tj = infer_type env t in
+      let u = univ_of_sort tj.utj_type in
+	(Universe.sup u lev, push_rel d env))
+    sign (Universe.type0m,env))
+
+let is_impredicative env u =
+  is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+
+let param_ccls params =
+  let has_some_univ u = function
+    | Some v when Univ.Level.equal u v -> true
+    | _ -> false
+  in
+  let remove_some_univ u = function
+    | Some v when Univ.Level.equal u v -> None
+    | x -> x
+  in
+  let fold l (_, b, p) = match b with
+  | None ->
+    (* Parameter contributes to polymorphism only if explicit Type *)
+    let c = strip_prod_assum p in
+    (* Add Type levels to the ordered list of parameters contributing to *)
+    (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
+    begin match kind_of_term c with
+    | Sort (Type u) ->
+      (match Univ.Universe.level u with
+      | Some u ->
+	if List.exists (has_some_univ u) l then
+          None :: List.map (remove_some_univ u) l
+	else
+          Some u :: l
+      | None -> None :: l)
+    | _ ->
+      None :: l
+    end
+  | _ -> l
+  in
+    List.fold_left fold [] params
 
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
+(* TODO check that we don't overgeneralize construcors/inductive arities with
+   universes that are absent from them. Is it possible? 
+*)
 let typecheck_inductive env mie =
-  if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
+  let () = match mie.mind_entry_inds with
+  | [] -> anomaly (Pp.str "empty inductive types declaration")
+  | _ -> ()
+  in
   (* Check unicity of names *)
   mind_check_names mie;
   (* Params are typed-checked here *)
-  let env_params, params, cst1 = infer_local_decls env mie.mind_entry_params in
+  let env' = push_context mie.mind_entry_universes env in
+  let (env_params, params) = 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 *)
+  (* This allows building the environment of arities and to share *)
   (* the set of constraints *)
-  let cst, env_arities, rev_arity_list =
+  let env_arities, rev_arity_list =
     List.fold_left
-      (fun (cst,env_ar,l) ind ->
+      (fun (env_ar,l) ind ->
          (* Arities (without params) are typed-checked here *)
-	 let arity, cst2 = infer_type env_params ind.mind_entry_arity in
+	 let expltype = ind.mind_entry_template in
+         let arity =
+	   if isArity ind.mind_entry_arity then
+	     let (ctx,s) = dest_arity env_params ind.mind_entry_arity in
+	       match s with
+	       | Type u when Univ.universe_level u = None ->
+	         (** We have an algebraic universe as the conclusion of the arity,
+		     typecheck the dummy Π ctx, Prop and do a special case for the conclusion.
+		 *)
+	         let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in
+		 let (cctx, _) = destArity proparity.utj_val in
+		   (* Any universe is well-formed, we don't need to check [s] here *)
+		   mkArity (cctx, s)
+	       | _ -> 
+		 let arity = infer_type env_params ind.mind_entry_arity in
+		   arity.utj_val
+	   else let arity = infer_type env_params ind.mind_entry_arity in
+		  arity.utj_val
+	 in
+	 let (sign, deflev) = dest_arity env_params arity in
+	 let inflev = 
+	   (* The level of the inductive includes levels of indices if 
+	      in indices_matter mode *)
+	     if !indices_matter 
+	     then Some (cumulate_arity_large_levels env_params sign)
+	     else None
+	 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 full_arity = it_mkProd_or_LetIn arity.utj_val params in
-	 let cst = union_constraints cst cst2 in
+	 let full_arity = it_mkProd_or_LetIn arity params in
 	 let id = ind.mind_entry_typename in
 	 let env_ar' =
-           push_rel (Name id, None, full_arity)
-             (add_constraints cst2 env_ar) in
-	 let lev =
-	   (* Decide that if the conclusion is not explicitly Type *)
-	   (* then the inductive type is not polymorphic *)
-	   match kind_of_term ((strip_prod_assum arity.utj_val)) with
-	   | Sort (Type u) -> Some u
-	   | _ -> None in
-         (cst,env_ar',(id,full_arity,lev)::l))
-      (cst1,env,[])
+           push_rel (Name id, None, full_arity) env_ar in
+             (* (add_constraints cst2 env_ar) in *)
+	   (env_ar', (id,full_arity,sign @ params,expltype,deflev,inflev)::l))
+      (env',[])
       mie.mind_entry_inds in
 
   let arity_list = List.rev rev_arity_list in
 
   (* builds the typing context "Gamma, I1:A1, ... In:An, params" *)
-  let env_ar_par =
-    push_rel_context params (add_constraints cst1 env_arities) in
+  let env_ar_par = push_rel_context params env_arities in
 
   (* Now, we type the constructors (without params) *)
-  let inds,cst =
+  let inds =
     List.fold_right2
-      (fun ind arity_data (inds,cst) ->
-	 let (info,lc',cstrs_univ,cst') =
-	   infer_constructor_packet env_ar_par params ind.mind_entry_lc in
+      (fun ind arity_data inds ->
+	 let (lc',cstrs_univ) =
+	   infer_constructor_packet env_ar_par ContextSet.empty
+	     params ind.mind_entry_lc in
 	 let consnames = ind.mind_entry_consnames in
-	 let ind' = (arity_data,consnames,info,lc',cstrs_univ) in
-	 (ind'::inds, union_constraints cst cst'))
+	 let ind' = (arity_data,consnames,lc',cstrs_univ) in
+	   ind'::inds)
       mie.mind_entry_inds
       arity_list
-      ([],cst) in
+    ([]) in
 
   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
-      (* Parameter contributes to polymorphism only if explicit Type *)
-      let c = strip_prod_assum p in
-      (* Add Type levels to the ordered list of parameters contributing to *)
-      (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
-      match kind_of_term c with
-      | Sort (Type u) ->
-          if List.mem (Some u) l then
-            None :: List.map (function Some v when u = v -> None | x -> x) l
-          else
-            Some u :: l
-      | _ ->
-          None :: l
-    else
-      l) [] params in
 
   (* Compute/check the sorts of the inductive types *)
-  let ind_min_levels = inductive_levels arities inds in
-  let inds, cst =
-    array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
-      let sign, s =
-        try dest_arity env full_arity
-        with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
+
+  let inds =
+    Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,(is_unit,clev))  ->
+      let infu = 
+	(** Inferred level, with parameters and constructors. *)
+	match inf_level with
+	| Some alev -> Universe.sup clev alev
+	| None -> clev
+      in
+      let full_polymorphic () = 
+	let defu = Term.univ_of_sort def_level in
+	let is_natural =
+	  type_in_type env || (check_leq (universes env') infu defu &&
+	    not (is_type0m_univ defu && not is_unit))
+	in
+	let _ =
+	  (** Impredicative sort, always allow *)
+	  if is_impredicative env defu then ()
+	  else (** Predicative case: the inferred level must be lower or equal to the
+		   declared level. *)
+	    if not is_natural then
+	      anomaly ~label:"check_inductive" 
+		(Pp.str"Incorrect universe " ++
+		   Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is "
+		 ++ Universe.pr infu)
+	in
+	  RegularArity (not is_natural,full_arity,defu)
+      in
+      let template_polymorphic () =
+	let sign, s =
+          try dest_arity env full_arity
+          with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
+	in
+	  match s with
+	  | Type u when expltype (* Explicitly polymorphic *) ->
+	    (* The polymorphic level is a function of the level of the *)
+	    (* conclusions of the parameters *)
+            (* We enforce [u >= lev] in case [lev] has a strict upper *)
+            (* constraints over [u] *)
+	    let b = type_in_type env || check_leq (universes env') infu u in
+	      if not b then
+		anomaly ~label:"check_inductive" 
+		  (Pp.str"Incorrect universe " ++
+		     Universe.pr u ++ Pp.str " declared for inductive type, inferred level is "
+		   ++ Universe.pr clev)
+	      else
+		TemplateArity (param_ccls params, infu)
+	  | _ (* Not an explicit occurrence of Type *) ->
+	    full_polymorphic ()
+      in
+      let arity = 
+	if mie.mind_entry_polymorphic then full_polymorphic ()
+	else template_polymorphic ()
       in
-      let status,cst = match s with
-      | Type u when ar_level <> None (* Explicitly polymorphic *)
-            && no_upper_constraints u cst ->
-	  (* The polymorphic level is a function of the level of the *)
-	  (* conclusions of the parameters *)
-          (* We enforce [u >= lev] in case [lev] has a strict upper *)
-          (* constraints over [u] *)
-	  Inr (param_ccls, lev), enforce_geq u lev cst
-      | Type u (* Not an explicit occurrence of Type *) ->
-	  Inl (info,full_arity,s), enforce_geq u lev cst
-      | Prop Pos when engagement env <> Some ImpredicativeSet ->
-	  (* Predicative set: check that the content is indeed predicative *)
-	  if not (is_type0m_univ lev) & not (is_type0_univ lev) then
-	    raise (InductiveError LargeNonPropInductiveNotInType);
-	  Inl (info,full_arity,s), cst
-      | Prop _ ->
-	  Inl (info,full_arity,s), cst in
-      (id,cn,lc,(sign,status)),cst)
-      inds ind_min_levels cst in
-
-  (env_arities, params, inds, cst)
+	(id,cn,lc,(sign,arity)))
+    inds
+  in (env_arities, params, inds)
 
 (************************************************************************)
 (************************************************************************)
@@ -321,11 +387,11 @@ let failwith_non_pos n ntypes c =
 
 let failwith_non_pos_vect n ntypes v =
   Array.iter (failwith_non_pos n ntypes) v;
-  anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur"
+  anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur")
 
 let failwith_non_pos_list n ntypes l =
   List.iter (failwith_non_pos n ntypes) l;
-  anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur"
+  anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur")
 
 (* Check the inductive type is called with the expected parameters *)
 let check_correct_par (env,n,ntypes,_) hyps l largs =
@@ -333,17 +399,17 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
   let largs = Array.of_list largs in
   if Array.length largs < nparams then
     raise (IllFormedInd (LocalNotEnoughArgs l));
-  let (lpar,largs') = array_chop nparams largs in
+  let (lpar,largs') = Array.chop nparams largs in
   let nhyps = List.length hyps in
   let rec check k index = function
     | [] -> ()
     | (_,Some _,_)::hyps -> check k (index+1) hyps
     | _::hyps ->
         match kind_of_term (whd_betadeltaiota env lpar.(k)) with
-	  | Rel w when w = index -> check (k-1) (index+1) hyps
+	  | Rel w when Int.equal w index -> check (k-1) (index+1) hyps
 	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
   in check (nparams-1) (n-nhyps) hyps;
-  if not (array_for_all (noccur_between n ntypes) largs') then
+  if not (Array.for_all (noccur_between n ntypes) largs') then
     failwith_non_pos_vect n ntypes largs'
 
 (* Computes the maximum number of recursive parameters :
@@ -352,9 +418,9 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     recursive parameters *)
 
 let compute_rec_par (env,n,_,_) hyps nmr largs =
-if nmr = 0 then 0 else
+if Int.equal nmr 0 then 0 else
 (* start from 0, hyps will be in reverse order *)
-  let (lpar,_) = list_chop nmr largs in
+  let (lpar,_) = List.chop nmr largs in
   let rec find k index =
       function
 	  ([],_) -> nmr
@@ -362,27 +428,10 @@ if nmr = 0 then 0 else
 	| (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps)
 	| (p::lp,_::hyps) ->
        ( match kind_of_term (whd_betadeltaiota env p) with
-	  | Rel w when w = index -> find (k+1) (index-1) (lp,hyps)
+	  | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,hyps)
           | _ -> k)
   in find 0 (n-1) (lpar,List.rev hyps)
 
-let lambda_implicit_lift n a =
-  let implicit_sort = mkType (make_univ (make_dirpath [id_of_string "implicit"], 0)) in
-  let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
-  iterate lambda_implicit n (lift n a)
-
-(* This removes global parameters of the inductive types in lc (for
-   nested inductive types only ) *)
-let abstract_mind_lc env ntyps npars lc =
-  if npars = 0 then
-    lc
-  else
-    let make_abs =
-      list_tabulate
-	(function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps
-    in
-    Array.map (substl make_abs) lc
-
 (* [env] is the typing environment
    [n] is the dB of the last inductive type
    [ntypes] is the number of inductive types in the definition
@@ -392,12 +441,13 @@ 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 specif = (lookup_mind_specif env mi, u) in
+  let ty = type_of_inductive env specif in
   let env' =
     push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive env specif) lpar) env in
+              hnf_prod_applist env ty 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
@@ -406,7 +456,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
   (env', newidx, ntypes, ra_env')
 
 let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
-  if n=0 then (ienv,c) else
+  if Int.equal n 0 then (ienv,c) else
     let c' = whd_betadeltaiota env c in
     match kind_of_term c' with
 	Prod(na,a,b) ->
@@ -414,7 +464,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
 	  ienv_decompose_prod ienv' (n-1) b
       | _ -> assert false
 
-let array_min nmr a = if nmr = 0 then 0 else
+let array_min nmr a = if Int.equal nmr 0 then 0 else
   Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a
 
 (* The recursive function that checks positivity and builds the list
@@ -427,7 +477,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
     let x,largs = decompose_app (whd_betadeltaiota env c) in
       match kind_of_term x with
 	| Prod (na,b,d) ->
-	    assert (largs = []);
+	    let () = assert (List.is_empty largs) in
             (match weaker_noccur_between env n ntypes b with
 		None -> failwith_non_pos_list n ntypes [b]
               | Some b ->
@@ -455,12 +505,12 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	    else failwith_non_pos_list n ntypes (x::largs)
 
   (* accesses to the environment are not factorised, but is it worth? *)
-  and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr (mi, largs) =
+  and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((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
     let (lpar,auxlargs) =
-      try list_chop auxnpar largs
+      try List.chop auxnpar largs
       with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
       (* If the inductive appears in the args (non params) then the
 	 definition is not positive. *)
@@ -469,12 +519,12 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	failwith_non_pos_list n ntypes auxlargs;
       (* We do not deal with imbricated mutual inductive types *)
       let auxntyp = mib.mind_ntypes in
-	if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
+	if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n));
 	(* The nested inductive type with parameters removed *)
-	let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
+	let auxlcvect = abstract_mind_lc 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_nmr =
@@ -503,25 +553,27 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	match kind_of_term x with
 
           | Prod (na,b,d) ->
-	      assert (largs = []);
+	      let () = assert (List.is_empty largs) in
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
-		check_constr_rec ienv' nmr' (recarg::lrec) d
-
-	  | hd ->
-	      if check_head then
-		if hd = Rel (n+ntypes-i-1) then
-		  check_correct_par ienv hyps (ntypes-i) largs
-		else
-		  raise (IllFormedInd LocalNotConstructor)
-	      else
-		if not (List.for_all (noccur_between n ntypes) largs)
-		then failwith_non_pos_list n ntypes largs;
-	      (nmr,List.rev lrec)
+                check_constr_rec ienv' nmr' (recarg::lrec) d
+          | hd ->
+            let () =
+              if check_head then
+                begin match hd with
+                | Rel j when Int.equal j (n + ntypes - i - 1) ->
+                  check_correct_par ienv hyps (ntypes - i) largs
+                | _ -> raise (IllFormedInd LocalNotConstructor)
+                end
+              else
+                if not (List.for_all (noccur_between n ntypes) largs)
+                then failwith_non_pos_list n ntypes largs
+            in
+            (nmr, List.rev lrec)
     in check_constr_rec ienv nmr [] c
   in
   let irecargs_nmr =
-    array_map2
+    Array.map2
       (fun id c ->
         let _,rawc = mind_extract_params lparams c in
           try
@@ -537,12 +589,12 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 let check_positivity kn env_ar params inds =
   let ntypes = Array.length inds in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
-  let lra_ind = List.rev (Array.to_list rc) in
+  let lra_ind = Array.rev_to_list rc in
   let lparams = rel_context_length params in
   let nmr = rel_context_nhyps params in
   let check_one i (_,lcnames,lc,(sign,_)) =
     let ra_env =
-      list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+      List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     let nargs = rel_context_nhyps sign - nmr in
     check_positivity_one ienv params (kn,i) nargs lcnames lc
@@ -563,67 +615,143 @@ let all_sorts = [InProp;InSet;InType]
 let small_sorts = [InProp;InSet]
 let logical_sorts = [InProp]
 
-let allowed_sorts issmall isunit s =
-  match family_of_sort s with
-  (* Type: all elimination allowed *)
-  | InType -> all_sorts
-
-  (* Small Set is predicative: all elimination allowed *)
-  | InSet when issmall -> all_sorts
-
-  (* Large Set is necessarily impredicative: forbids large elimination *)
-  | 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 *)
-  | InProp when isunit -> if issmall then all_sorts else small_sorts
-
-  (* Other propositions: elimination only to Prop *)
-  | InProp -> logical_sorts
+let allowed_sorts is_smashed s =
+  if not is_smashed 
+  then (** Naturally in the defined sort.
+	   If [s] is Prop, it must be small and unitary.
+	   Unsmashed, predicative Type and Set: all elimination allowed
+	   as well. *)
+      all_sorts
+  else 
+    match family_of_sort s with
+    (* Type: all elimination allowed: above and below *)
+    | InType -> all_sorts
+    (* Smashed Set is necessarily impredicative: forbids large elimination *)
+    | InSet -> small_sorts
+    (* Smashed to Prop, no informative eliminations allowed *)
+    | InProp -> logical_sorts
+    
+(* Previous comment: *)
+(* Unitary/empty Prop: elimination to all sorts are realizable *)
+(* unless the type is large. If it is large, forbids large elimination *)
+(* which otherwise allows simulating the inconsistent system Type:Type. *)
+(* -> this is now handled by is_smashed: *)
+(* - all_sorts in case of small, unitary Prop (not smashed) *)
+(* - logical_sorts in case of large, unitary Prop (smashed) *)
+
+let arity_conclusion = function
+  | RegularArity (_, c, _) -> c
+  | TemplateArity (_, s) -> mkType s
 
 let fold_inductive_blocks f =
-  Array.fold_left (fun acc (_,_,lc,(arsign,_)) ->
-    f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (* dummy *) mkSet arsign))
+  Array.fold_left (fun acc (_,_,lc,(arsign,ar)) ->
+    f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (arity_conclusion ar) arsign))
 
 let used_section_variables env inds =
   let ids = fold_inductive_blocks
-    (fun l c -> Idset.union (Environ.global_vars_set env c) l)
-      Idset.empty inds in
+    (fun l c -> Id.Set.union (Environ.global_vars_set env c) l)
+      Id.Set.empty inds in
   keep_hyps env ids
 
-let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
+let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
+let rel_appvect n m = rel_vect n (List.length m)
+
+exception UndefinableExpansion
+
+(** From a rel context describing the constructor arguments,
+    build an expansion function.
+    The term built is expecting to be substituted first by 
+    a substitution of the form [params, x : ind params] *)
+let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
+    mind_consnrealdecls mind_consnrealargs ctx =
+  let mp, dp, l = repr_mind kn in
+  let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
+  let ci = 
+    let print_info =
+      { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
+      { ci_ind     = ind;
+	ci_npar    = nparamargs;
+	ci_cstr_ndecls = mind_consnrealdecls;
+	ci_cstr_nargs = mind_consnrealargs;
+	ci_pp_info = print_info }
+  in
+  let len = List.length ctx in
+  let x = Name x in
+  let compat_body ccl i = 
+    (* [ccl] is defined in context [params;x:rp] *)
+    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+    let ccl' = liftn 1 2 ccl in
+    let p = mkLambda (x, lift 1 rp, ccl') in
+    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
+    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
+      it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params
+  in
+  let projections (na, b, t) (i, j, kns, pbs, subst) =
+    match b with
+    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst)
+    | None ->
+      match na with
+      | Name id ->
+	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+	let ty = substl subst (liftn 1 j t) in
+	let term = mkProj (Projection.make kn true, mkRel 1) in
+	let fterm = mkProj (Projection.make kn false, mkRel 1) in
+	let compat = compat_body ty (j - 1) in
+	let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
+	let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
+	let body = { proj_ind = fst ind; proj_npars = nparamargs;
+		     proj_arg = i; proj_type = ty; proj_eta = etab, etat; 
+		     proj_body = compat } in
+	  (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
+      | Anonymous -> raise UndefinableExpansion
+  in
+  let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
+    Array.of_list (List.rev kns),
+    Array.of_list (List.rev pbs)
+
+let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
-  let hyps =  used_section_variables env inds in
+  let hyps = used_section_variables env inds in
   let nparamargs = rel_context_nhyps params in
   let nparamdecls = rel_context_length params in
+  let subst, ctx = Univ.abstract_universes p ctx in
+  let params = Vars.subst_univs_level_context subst params in
+  let env_ar = 
+    let ctx = Environ.rel_context env_ar in 
+    let ctx' = Vars.subst_univs_level_context subst ctx in
+      Environ.push_rel_context ctx' env
+  in
   (* Check one inductive *)
   let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
     (* Type of constructors in normal form *)
+    let lc = Array.map (Vars.subst_univs_level_constr subst) lc in
     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
-    let consnrealargs =
+    let consnrealdecls =
       Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
 	splayed_lc in
+    let consnrealargs =
+      Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params)
+	splayed_lc in
     (* Elimination sorts *)
-    let arkind,kelim = match ar_kind with
-      | Inr (param_levels,lev) ->
-	  Polymorphic {
-	      poly_param_levels = param_levels;
-	      poly_level = lev;
-	    }, all_sorts
-      | Inl ((issmall,isunit),ar,s) ->
-	  let kelim = allowed_sorts issmall isunit s in
-	    Monomorphic {
-		mind_user_arity = ar;
-		mind_sort = s;
-	      }, kelim in
+    let arkind,kelim = 
+      match ar_kind with
+      | TemplateArity (paramlevs, lev) -> 
+	let ar = {template_param_levels = paramlevs; template_level = lev} in
+	  TemplateArity ar, all_sorts
+      | RegularArity (info,ar,defs) ->
+	let s = sort_of_univ defs in
+	let kelim = allowed_sorts info s in
+	let ar = RegularArity 
+	  { mind_user_arity = Vars.subst_univs_level_constr subst ar; 
+	    mind_sort = sort_of_univ (Univ.subst_univs_level_universe subst defs); } in
+	  ar, kelim in
     (* Assigning VM tags to constructors *)
     let nconst, nblock = ref 0, ref 0 in
     let transf num =
       let arity = List.length (dest_subterms recarg).(num) in
-	if arity = 0 then
+	if Int.equal arity 0 then
 	  let p  = (!nconst, 0) in
 	    incr nconst; p
 	else
@@ -636,12 +764,13 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
       (* Build the inductive packet *)
       { mind_typename = id;
 	mind_arity = arkind;
-	mind_arity_ctxt = ar_sign;
+	mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign;
 	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
-	mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls;
+	mind_nrealdecls = rel_context_length ar_sign - nparamdecls;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
-	mind_consnrealdecls = consnrealargs;
+	mind_consnrealdecls = consnrealdecls;
+	mind_consnrealargs = consnrealargs;
 	mind_user_lc = lc;
 	mind_nf_lc = nf_lc;
 	mind_recargs = recarg;
@@ -649,7 +778,30 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	mind_nb_args = !nblock;
 	mind_reloc_tbl = rtbl;
       } in
-  let packets = array_map2 build_one_packet inds recargs in
+  let packets = Array.map2 build_one_packet inds recargs in
+  let pkt = packets.(0) in	  
+  let isrecord = 
+    match isrecord with
+    | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1
+			   && pkt.mind_consnrealargs.(0) > 0 ->
+      (** The elimination criterion ensures that all projections can be defined. *)
+      let u = 
+	if p then 
+	  subst_univs_level_instance subst (Univ.UContext.instance ctx)
+	else Univ.Instance.empty 
+      in
+      let indsp = ((kn, 0), u) in
+      let rctx, _ = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
+	(try 
+	   let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
+	   let kns, projs = 
+	     compute_projections indsp pkt.mind_typename rid nparamargs params
+	       pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
+	   in Some (Some (rid, kns, projs))
+	 with UndefinableExpansion -> Some None)
+    | Some _ -> Some None
+    | None -> None
+  in
     (* Build the mutual inductive *)
     { mind_record = isrecord;
       mind_ntypes = ntypes;
@@ -659,7 +811,9 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
       mind_nparams_rec = nmr;
       mind_params_ctxt = params;
       mind_packets = packets;
-      mind_constraints = cst
+      mind_polymorphic = p;
+      mind_universes = ctx;
+      mind_private = prv;
     }
 
 (************************************************************************)
@@ -667,9 +821,11 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar, params, inds, cst) = typecheck_inductive env mie in
+  let (env_ar, params, inds) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
   let (nmr,recargs) = check_positivity kn env_ar params inds in
   (* Build the inductive packets *)
-    build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
-      inds nmr recargs cst
+    build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
+      mie.mind_entry_universes
+      env_ar params kn mie.mind_entry_record mie.mind_entry_finite
+      inds nmr recargs