Imported Upstream version 8.9.0upstream/8.9.0upstream

21 files changed, 247 insertions, 240 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index f79ba66e..139fa765 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -3,7 +3,6 @@ Coq_config
 Analyze
 Hook
 Terminal
-Canary
 Hashset
 Hashcons
 CSet
diff --git a/checker/checker.ml b/checker/checker.ml
index fd2725c8..d63575b3 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -243,7 +243,9 @@ let explain_exn = function
   | Invalid_argument s ->
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ())
   | Sys.Break ->
-      hov 0 (fnl () ++ str "User interrupt.")
+    hov 0 (fnl () ++ str "User interrupt.")
+  | Univ.AlreadyDeclared ->
+    hov 0 (str "Error: Multiply declared universe.")
   | Univ.UniverseInconsistency (o,u,v) ->
       let msg =
 	if !Flags.debug (*!Constrextern.print_universes*) then
diff --git a/checker/cic.mli b/checker/cic.mli
index c4b00d0d..17259bb4 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -33,11 +33,10 @@ open Names
 
 (** {6 The sorts of CCI. } *)
 
-type contents = Pos | Null
-
 type sorts =
-  | Prop of contents       (** Prop and Set *)
-  | Type of Univ.universe  (** Type *)
+  | Prop
+  | Set
+  | Type of Univ.universe
 
 (** {6 The sorts family of CCI. } *)
 
@@ -128,7 +127,7 @@ type section_context = unit
 (** {6 Substitutions} *)
 
 type delta_hint =
-  | Inline of int * constr option
+  | Inline of int * (Univ.AUContext.t * constr) option
   | Equiv of KerName.t
 
 type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
@@ -203,18 +202,6 @@ 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 : MutInd.t;
-  proj_npars : int;
-  proj_arg : int;
-  proj_type : constr; (* Type under params *)
-  proj_eta : constr * constr; (* Eta-expanded term and type *)
-  proj_body : constr; (* For compatibility, the match version *)
-}
-
 type constant_def =
   | Undef of inline
   | Def of constr_substituted
@@ -233,6 +220,7 @@ type typing_flags = {
                             points are assumed to be total. *)
   check_universes : bool; (** If [false] universe constraints are not checked *)
   conv_oracle : oracle; (** Unfolding strategies for conversion *)
+  share_reduction : bool; (** Use by-need reduction algorithm *)
 }
 
 type constant_body = {
@@ -241,7 +229,6 @@ type constant_body = {
     const_type : constr;
     const_body_code : to_patch_substituted;
     const_universes : constant_universes;
-    const_proj : projection_body option;
     const_inline_code : bool;
     const_typing_flags : typing_flags;
 }
@@ -255,9 +242,10 @@ type recarg =
 
 type wf_paths = recarg Rtree.t
 
-type record_body = (Id.t * Constant.t array * projection_body array) option
-    (* The body is empty for non-primitive records, otherwise we get its
-       binder name in projections and list of projections if it is primitive. *)
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Label.t array * constr array) array
 
 type regular_inductive_arity = {
   mind_user_arity : constr;
@@ -325,7 +313,7 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : record_body option; (** Whether the inductive type has been declared as a record. *)
+    mind_record : record_info; (** Whether the inductive type has been declared as a record. *)
 
     mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
diff --git a/checker/closure.ml b/checker/closure.ml
index b9ae4daa..57060116 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -273,7 +273,7 @@ let update v1 (no,t) =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Projection.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -497,8 +497,8 @@ let rec zip m stk =
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
-    | Zproj (i,j,cst) :: s -> 
-        zip {norm=neutr m.norm; term=FProj (cst,m)} s
+    | Zproj p :: s ->
+        zip {norm=neutr m.norm; term=FProj (Projection.make p true,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
     | Zshift(n)::s ->
@@ -618,20 +618,25 @@ let drop_parameters depth n argstk =
 
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
-    match mib.mind_record with
-    | Some (Some (_,projs,pbs)) when mib.mind_finite <> CoFinite -> 
-	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
-	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
-      let pars = mib.mind_nparams in
-      let right = fapp_stack (f, s') in
-      let (depth, args, s) = strip_update_shift_app m s in
-      (** Try to drop the params, might fail on partially applied constructors. *)
-      let argss = try_drop_parameters depth pars args in
-	let hstack =
-	  Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-			     term = FProj (Projection.make p false, right) }) projs in
-	argss, [Zapp hstack]	
-    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+  (* disallow eta-exp for non-primitive records *)
+  if not (mib.mind_finite == BiFinite) then raise Not_found;
+  match Declarations.inductive_make_projections ind mib with
+  | Some projs ->
+    (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+       arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
+    let pars = mib.mind_nparams in
+    let right = fapp_stack (f, s') in
+    let (depth, args, s) = strip_update_shift_app m s in
+    (** Try to drop the params, might fail on partially applied constructors. *)
+    let argss = try_drop_parameters depth pars args in
+    let hstack =
+      Array.map (fun p ->
+          { norm = Red; (* right can't be a constructor though *)
+            term = FProj (Projection.make p false, right) })
+        projs
+    in
+    argss, [Zapp hstack]
+  | None -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
@@ -668,8 +673,7 @@ let contract_fix_vect fix =
   (subs_cons(Array.init nfix make_body, env), thisbody)
 
 let unfold_projection env p =
-  let pb = lookup_projection p env in
-  Zproj (pb.proj_npars, pb.proj_arg, p)
+  Zproj (Projection.repr p)
 
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
@@ -747,9 +751,9 @@ 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
+       | (depth, args, Zproj p::s) ->
+            let rargs = drop_parameters depth (Projection.Repr.npars p) args in
+            let rarg = project_nth_arg (Projection.Repr.arg p) rargs in
 	    kni info rarg s
        | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
diff --git a/checker/closure.mli b/checker/closure.mli
index 49b07f73..cec78569 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -103,7 +103,7 @@ type fterm =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Projection.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index d2c3f203..0540227c 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -196,7 +196,12 @@ let subst_con0 sub con u =
   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', subst_instance_constr u t
+    | Some (ctx, t) ->
+      (** FIXME: we never typecheck the inlined term, so that it could well
+          be garbage. What environment do we type it in though? The substitution
+          code should be moot in the checker but it **is** used nonetheless. *)
+      let () = assert (Univ.AUContext.size ctx == Univ.Instance.length u) in
+      con', subst_instance_constr u t
     | None ->
       let con'' = match side with
 	| User -> constant_of_delta resolve con'
@@ -209,11 +214,7 @@ let rec map_kn f f' c =
     match c with
       | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
       | Proj (p,t) -> 
-          let p' = 
-	    Projection.map (fun kn ->
-			    try fst (f' kn Univ.Instance.empty)
-			    with No_subst -> kn) p
-	  in
+          let p' = Projection.map f p in
 	  let t' = func t in
 	    if p' == p && t' == t then c
 	    else Proj (p', t')
@@ -231,7 +232,7 @@ let rec map_kn f f' c =
 	  in
 	  let p' = func p in
 	  let ct' = func ct in
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (ci.ci_ind==ci_ind && p'==p
 		&& l'==l && ct'==ct)then c
 	    else
@@ -260,21 +261,21 @@ let rec map_kn f f' c =
 	    else LetIn (na, b', t', ct')
       | App (ct,l) ->
 	  let ct' = func ct in
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (ct'== ct && l'==l) then c
 	    else App (ct',l')
       | Evar (e,l) ->
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (l'==l) then c
 	    else Evar (e,l')
       | Fix (ln,(lna,tl,bl)) ->
-	  let tl' = Array.smartmap func tl in
-	  let bl' = Array.smartmap func bl in
+          let tl' = Array.Smart.map func tl in
+          let bl' = Array.Smart.map func bl in
 	    if (bl == bl'&& tl == tl') then c
 	    else Fix (ln,(lna,tl',bl'))
       | CoFix(ln,(lna,tl,bl)) ->
-	  let tl' = Array.smartmap func tl in
-	  let bl' = Array.smartmap func bl in
+          let tl' = Array.Smart.map func tl in
+          let bl' = Array.Smart.map func bl in
 	    if (bl == bl'&& tl == tl') then c
 	    else CoFix (ln,(lna,tl',bl'))
       | _ -> c
@@ -340,7 +341,7 @@ let gen_subst_delta_resolver dom subst resolver =
     let kkey' = if dom then subst_kn subst kkey else kkey in
     let hint' = match hint with
       | Equiv kequ -> Equiv (subst_kn_delta subst kequ)
-      | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+      | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
       | Inline (_,None) -> hint
     in
     Deltamap.add_kn kkey' hint' rslv
@@ -480,7 +481,7 @@ let dest_subterms p =
   let (_,cstrs) = Rtree.dest_node p in
   Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
 
-let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p
 
 let eq_recarg r1 r2 = match r1, r2 with
   | Norec, Norec -> true
@@ -490,6 +491,16 @@ let eq_recarg r1 r2 = match r1, r2 with
 
 let eq_wf_paths = Rtree.equal eq_recarg
 
+let inductive_make_projections ind mib =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    let projs = Array.mapi (fun proj_arg lab ->
+        Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab)
+        (pi2 infos.(snd ind))
+    in
+    Some projs
+
 (**********************************************************************)
 (* Representation of mutual inductive types in the kernel             *)
 (*
@@ -513,7 +524,7 @@ let subst_decl_arity f g sub ar =
 let subst_rel_declaration sub =
   Term.map_rel_decl (subst_mps sub)
 
-let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
+let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub)
 
 let constant_is_polymorphic cb =
   match cb.const_universes with
@@ -544,10 +555,10 @@ let subst_mind_packet sub mbp =
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_consnrealargs = mbp.mind_consnrealargs;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
+    mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_ind_arity sub mbp.mind_arity;
-    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
+    mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealdecls = mbp.mind_nrealdecls;
     mind_kelim = mbp.mind_kelim;
@@ -560,7 +571,7 @@ let subst_mind_packet sub mbp =
 let subst_mind sub mib =
   { mib with
     mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt;
-    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets }
+    mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets }
 
 (* Modules *)
 
@@ -599,7 +610,7 @@ and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generi
     mod_mp = subst_mp sub mb.mod_mp;
     mod_expr = subst_impl sub mb.mod_expr;
     mod_type = subst_signature sub mb.mod_type;
-    mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
+    mod_type_alg = Option.Smart.map (subst_expression sub) mb.mod_type_alg }
 
 and subst_module sub mb =
   subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 7458b3e0..ce852644 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -25,6 +25,9 @@ val dest_subterms : wf_paths -> wf_paths list array
 val eq_recarg : recarg -> recarg -> bool
 val eq_wf_paths : wf_paths -> wf_paths -> bool
 
+val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
+  Names.Projection.Repr.t array option
+
 (* Modules *)
 
 val empty_delta_resolver : delta_resolver
diff --git a/checker/environ.ml b/checker/environ.ml
index bbd043c8..b172acb1 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -164,14 +164,6 @@ let evaluable_constant cst env =
   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 p env =
-  match (lookup_constant (Projection.constant p) env).const_proj with 
-  | Some pb -> pb
-  | None -> anomaly ("lookup_projection: constant is not a projection.")
-
 (* Mutual Inductives *)
 let scrape_mind env kn=
   try
@@ -191,7 +183,7 @@ let lookup_mind kn env =
 
 let add_mind kn mib env =
   if Mindmap_env.mem kn env.env_globals.env_inductives then
-    Printf.ksprintf anomaly ("Inductive %s is already defined.")
+    Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.")
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
@@ -201,10 +193,23 @@ let add_mind kn mib env =
     KNmap.add kn1 kn2  env.env_globals.env_inductives_eq in
   let new_globals =
     { env.env_globals with
-	env_inductives = new_inds;
-	env_inductives_eq = new_inds_eq} in
+      env_inductives = new_inds;
+      env_inductives_eq = new_inds_eq} in
   { env with env_globals = new_globals }
 
+let lookup_projection p env =
+  let mind,i = Projection.inductive p in
+  let mib = lookup_mind mind env in
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> CErrors.anomaly ~label:"lookup_projection" Pp.(str "not a projection")
+  | PrimRecord infos ->
+    let _,labs,typs = infos.(i) in
+    let parg = Projection.arg p in
+    if not (Label.equal labs.(parg) (Projection.label p))
+    then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect label on projection")
+    else if not (Int.equal mib.mind_nparams (Projection.npars p))
+    then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect param number on projection")
+    else typs.(parg)
 
 (* Modules *)
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 81da8387..af1b2a62 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -57,8 +57,8 @@ exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> Constant.t puniverses -> constr
 val evaluable_constant : Constant.t -> env -> bool
 
-val is_projection : Constant.t -> env -> bool
-val lookup_projection : Projection.t -> env -> projection_body
+(** NB: here in the checker we check the inferred info (npars, label) *)
+val lookup_projection : Projection.t -> env -> constr
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 916934a8..f36fef7f 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -107,11 +107,11 @@ let rec sorts_of_constr_args env t =
 
 (* Prop and Set are small *)
 let is_small_sort = function
-  | Prop _ -> true
+  | Prop | Set -> true
   | _ -> false
 
 let is_logic_sort = function
-| Prop Null -> true
+| Prop -> true
 | _ -> false
 
 (* [infos] is a sequence of pair [islogic,issmall] for each type in
@@ -186,10 +186,10 @@ let check_predicativity env s small level =
         (*     (universes env) in *)
         if not (Univ.check_leq (universes env) level u) then
           failwith "impredicative Type inductive type"
-    | Prop Pos, ImpredicativeSet -> ()
-    | Prop Pos, _ ->
+    | Set, ImpredicativeSet -> ()
+    | Set, _ ->
         if not small then failwith "impredicative Set inductive type"
-    | Prop Null,_ -> ()
+    | Prop,_ -> ()
 
 
 let sort_of_ind = function
@@ -221,7 +221,7 @@ let allowed_sorts issmall isunit s =
 
 
 
-let compute_elim_sorts env_ar params mib arity lc =
+let compute_elim_sorts env_ar params arity lc =
   let inst = extended_rel_list 0 params in
   let env_params = push_rel_context params env_ar in
   let lc = Array.map
@@ -239,7 +239,7 @@ let compute_elim_sorts env_ar params mib arity lc =
   allowed_sorts small unit s
 
 
-let typecheck_one_inductive env params mib mip =
+let typecheck_one_inductive env params mip =
   (* mind_typename and mind_consnames not checked *)
   (* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *)
   (* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *)
@@ -256,7 +256,7 @@ let typecheck_one_inductive env params mib mip =
   Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls;
   (* mind_kelim: checked by positivity criterion ? *)
   let sorts =
-    compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in
+    compute_elim_sorts env params mip.mind_arity mip.mind_nf_lc in
   let reject_sort s = not (List.mem_f family_equal s sorts) in
   if List.exists reject_sort mip.mind_kelim then
     failwith "elimination not allowed";
@@ -355,7 +355,7 @@ let lambda_implicit_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 =
+let abstract_mind_lc ntyps npars lc =
   if npars = 0 then
     lc
   else
@@ -448,7 +448,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
       let auxntyp = mib.mind_ntypes in
 	if 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,u),lpar) in
@@ -525,10 +525,11 @@ let check_positivity env_ar mind params nrecp inds =
     Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
+  let ra_env =
+    List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
+  let env_ar_par = push_rel_context params env_ar in
   let check_one i mip =
-    let ra_env =
-      List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
-    let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
+    let ienv = (env_ar_par, 1+lparams, ntypes, ra_env) in
       check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
   in
   let irecargs = Array.mapi check_one inds in
@@ -595,8 +596,12 @@ let check_subtyping cumi paramsctxt env inds =
 (************************************************************************)
 (************************************************************************)
 
+let print_mutind ind =
+  let kn = MutInd.user ind in
+  str (ModPath.to_string (KerName.modpath kn) ^ "." ^ Label.to_string (KerName.label kn))
+
 let check_inductive env kn mib =
-  Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
+  Flags.if_verbose Feedback.msg_notice (str "  checking mutind block: " ++ print_mutind kn);
   (* check mind_constraints: should be consistent with env *)
   let env0 =
     match mib.mind_universes with
@@ -625,7 +630,7 @@ let check_inductive env kn mib =
   (*  - check arities *)
   let env_ar = typecheck_arity env0 params mib.mind_packets in
   (*  - check constructor types *)
-  Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
+  Array.iter (typecheck_one_inductive env_ar params) mib.mind_packets;
   (* check the inferred subtyping relation *)
   let () = 
     match mib.mind_universes with
diff --git a/checker/inductive.ml b/checker/inductive.ml
index e1c6b135..46a859f0 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -101,7 +101,7 @@ let instantiate_params full t u args sign =
   substl subs ty
 
 let full_inductive_instantiate mib u params sign =
-  let dummy = Prop Null in
+  let dummy = Prop in
   let t = mkArity (Term.subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
@@ -137,8 +137,8 @@ Remark: Set (predicative) is encoded as Type(0)
 
 let sort_as_univ = function
 | Type u -> u
-| Prop Null -> Univ.type0m_univ
-| Prop Pos -> Univ.type0_univ
+| Prop -> Univ.type0m_univ
+| Set -> Univ.type0_univ
 
 (* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
 (* in the domain or add [u |-> sup x su] if [u] is already mapped *)
@@ -195,9 +195,9 @@ let instantiate_universes env ctx ar argsorts =
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
-    if Univ.is_type0m_univ level then Prop Null
+    if Univ.is_type0m_univ level then Prop
     (* Non singleton type not containing types are interpretable in Set *)
-    else if Univ.is_type0_univ level then Prop Pos
+    else if Univ.is_type0_univ level then Set
     (* This is a Type with constraints *)
     else Type level
   in
@@ -226,8 +226,8 @@ let type_of_inductive env mip =
 (* The max of an array of universes *)
 
 let cumulate_constructor_univ u = function
-  | Prop Null -> u
-  | Prop Pos -> Univ.sup Univ.type0_univ u
+  | Prop -> u
+  | Set -> Univ.sup Univ.type0_univ u
   | Type u' -> Univ.sup u u'
 
 let max_inductive_sort =
@@ -383,7 +383,7 @@ let type_case_branches env (pind,largs) (p,pj) c =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    not (eq_ind_chk indsp ci.ci_ind) ||
+    not (mind_equiv env indsp ci.ci_ind) ||
     (mib.mind_nparams <> ci.ci_npar) ||
     (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
     (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
@@ -797,7 +797,7 @@ let rec subterm_specif renv stack t =
 
       | Lambda (x,a,b) ->
           assert (l=[]);
-	  let spec,stack' = extract_stack renv a stack in
+          let spec,stack' = extract_stack stack in
 	    subterm_specif (push_var renv (x,a,spec)) stack' b
 
       (* Metas and evars are considered OK *)
@@ -813,7 +813,7 @@ and stack_element_specif = function
   |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
   |SArg x -> x
 
-and extract_stack renv a = function
+and extract_stack = function
   | [] -> Lazy.from_val Not_subterm , []
   | h::t -> stack_element_specif h, t
 
@@ -845,7 +845,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) =
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
 
-let filter_stack_domain env ci p stack =
+let filter_stack_domain env p stack =
   let absctx, ar = dest_lam_assum env p in
   (* Optimization: if the predicate is not dependent, no restriction is needed
      and we avoid building the recargs tree. *)
@@ -925,7 +925,7 @@ let check_one_fix renv recpos trees def =
             let case_spec = branches_specif renv 
 	      (lazy_subterm_specif renv [] c_0) ci in
 	    let stack' = push_stack_closures renv l stack in
-        let stack' = filter_stack_domain renv.env ci p stack' in
+        let stack' = filter_stack_domain renv.env p stack' in
               Array.iteri (fun k br' -> 
 			     let stack_br = push_stack_args case_spec.(k) stack' in
 			     check_rec_call renv stack_br br') lrest
@@ -968,7 +968,7 @@ let check_one_fix renv recpos trees def =
         | Lambda (x,a,b) ->
 	    assert (l = []);
 	    check_rec_call renv [] a ;
-	    let spec, stack' = extract_stack renv a stack in
+            let spec, stack' = extract_stack stack in
 	    check_rec_call (push_var renv (x,a,spec)) stack' b
 
         | Prod (x,a,b) ->
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 3ef2b340..6b2af71f 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,17 +26,12 @@ let check_constant_declaration env kn cb =
       push_context ~strict:false ctx env
   in
   let ty = cb.const_type in
-  let () = ignore(infer_type env' ty) in
-  let () = 
+  let _ = infer_type env' ty in
+  let () =
     match body_of_constant cb with
     | Some bd ->
-      (match cb.const_proj with 
-      | None -> let j = infer env' bd in
-                  conv_leq env' j ty
-      | Some pb -> 
-	let env' = add_constant kn cb env' in
-	let j = infer env' bd in
-          conv_leq env' j ty)
+      let j = infer env' bd in
+      conv_leq env' j ty
     | None -> ()
   in
   let env =
diff --git a/checker/modops.ml b/checker/modops.ml
index c7ad0977..b92d7bbf 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -80,7 +80,7 @@ and add_module mb env =
 
 let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env
 
-let strengthen_const mp_from l cb resolver =
+let strengthen_const mp_from l cb =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
@@ -104,34 +104,34 @@ and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a ge
   match mb.mod_type with
   | MoreFunctor _ -> mb
   | NoFunctor sign ->
-    let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
+    let resolve_out,sign_out = strengthen_sig mp_from sign mp_to
     in
     { mb with
       mod_expr = mk_expr mp_to;
       mod_type = NoFunctor sign_out;
       mod_delta = resolve_out }
 
-and strengthen_sig mp_from sign mp_to resolver =
+and strengthen_sig mp_from sign mp_to =
   match sign with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
-	let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+        let item' = l,SFBconst (strengthen_const mp_from l cb) in
+        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
 	resolve_out,item'::rest'
     | (_,SFBmind _ as item):: rest ->
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
 	  resolve_out,item::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot(mp_to,l) in
 	let mb_out = strengthen_mod mp_from' mp_to' mb in
 	let item' = l,SFBmodule (mb_out) in
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
 	resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
-	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest ->
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	resolve_out,item::rest'
+        item':: rest'
+    | (_,SFBmodtype _ as item) :: rest ->
+        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
+        resolve_out,item::rest'
 
 let strengthen mtb mp =
   strengthen_body ignore mtb.mod_mp mp mtb
diff --git a/checker/print.ml b/checker/print.ml
index fc9cd687..247c811f 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -57,8 +57,8 @@ let print_pure_constr fmt csr =
     fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c
 
   and pp_sort fmt = function
-    | Prop(Pos) -> pp_print_string fmt  "Set"
-    | Prop(Null) -> pp_print_string fmt "Prop"
+    | Set -> pp_print_string fmt  "Set"
+    | Prop -> pp_print_string fmt "Prop"
     | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u)
 
   and pp_name fmt = function
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 4e508dc7..ee16675e 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -43,7 +43,7 @@ let compare_stack_shape stk1 stk2 =
     | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
     | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
-    | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
+    | (Zproj p1::s1, Zproj p2::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
     | ((ZcaseT(c1,_,_,_))::s1,
        (ZcaseT(c2,_,_,_))::s2) ->
@@ -55,7 +55,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.Projection.t * lift
+  | Zlproj of Names.Projection.Repr.t * 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
@@ -74,8 +74,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)
+            | (Zproj p, (l,pstk)) ->
+                (l, Zlproj (p,l)::pstk)
             | (Zfix(fx,a),(l,pstk)) ->
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
@@ -133,7 +133,7 @@ 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 compare_stacks f fmind fproj lft1 stk1 lft2 stk2 =
   let rec cmp_rec pstk1 pstk2 =
     match (pstk1,pstk2) with
       | (z1::s1, z2::s2) ->
@@ -143,10 +143,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 f fx1 fx2; cmp_rec a1 a2
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-               if not (Names.Constant.UserOrd.equal
-		       (Names.Projection.constant c1)
-		       (Names.Projection.constant c2)) then 
-		raise NotConvertible
+               if not (fproj c1 c2) then
+                raise NotConvertible
             | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
 		  raise NotConvertible;
@@ -194,10 +192,7 @@ let convert_constructors
   | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
   | Cumulative_ind cumi ->
     let num_cnstr_args =
-      let nparamsctxt =
-        mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
-      in
-      nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
+      mind.mind_nparams + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
     in
     if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
       convert_universes univs u1 u2
@@ -210,29 +205,26 @@ let convert_constructors
 
 let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
-    | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
-    | (Prop c1, Type u)  ->
+  | Prop, Prop | Set, Set -> ()
+  | Prop, (Set | Type _) | Set, Type _ ->
+    if not (pb = CUMUL) then raise NotConvertible
+  | Type u1, Type u2 ->
+    (** FIXME: handle type-in-type option here *)
+    if (* snd (engagement env) == StratifiedType && *)
+      not
         (match pb with
-            CUMUL -> ()
-          | _ -> raise NotConvertible)
-    | (Type u1, Type u2) ->
-        (** FIXME: handle type-in-type option here *)
-        if (* snd (engagement env) == StratifiedType && *)
-          not
-	  (match pb with
-            | CONV -> Univ.check_eq univ u1 u2
-	    | CUMUL -> Univ.check_leq univ u1 u2)
-        then begin
-          if !Flags.debug then begin
-            let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-            Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
-               str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
-               ++ Univ.pr_universes univ)
-          end;
-          raise NotConvertible
-        end
-    | (_, _) -> raise NotConvertible
+         | CONV -> Univ.check_eq univ u1 u2
+         | CUMUL -> Univ.check_leq univ u1 u2)
+    then begin
+      if !Flags.debug then begin
+        let op = match pb with CONV -> "=" | CUMUL -> "<=" in
+        Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+            str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+            ++ Univ.pr_universes univ)
+      end;
+      raise NotConvertible
+    end
+  | Set, Prop | Type _, (Prop | Set) -> raise NotConvertible
 
 let rec no_arg_available = function
   | [] -> true
@@ -260,7 +252,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
+  | Zproj _ :: _ -> false
   | ZcaseT _ :: _ -> false
   | Zfix _ :: _ -> true
 
@@ -303,6 +295,10 @@ let eq_table_key univ =
       Constant.UserOrd.equal c1 c2 &&
       Univ.Instance.check_eq univ u1 u2)
 
+let proj_equiv_infos infos p1 p2 =
+  Int.equal (Projection.Repr.arg p1) (Projection.Repr.arg p2) &&
+  mind_equiv (infos_env infos) (Projection.Repr.inductive p1) (Projection.Repr.inductive p2)
+
 (* 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,[]))
@@ -526,7 +522,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 and convert_stacks univ infos lft1 lft2 stk1 stk2 =
   compare_stacks
     (fun (l1,t1) (l2,t2) -> ccnv univ CONV infos l1 l2 t1 t2)
-    (mind_equiv_infos infos)
+    (mind_equiv_infos infos) (proj_equiv_infos infos)
     lft1 stk1 lft2 stk2
 
 and convert_vect univ infos lft1 lft2 v1 v2 =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 31dab0c9..0916d98d 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -12,7 +12,6 @@
 open Util
 open Names
 open Cic
-open Term
 open Declarations
 open Environ
 open Reduction
@@ -123,16 +122,6 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       env, Univ.make_abstract_instance auctx'
     | _ -> error ()
   in
-  let eq_projection_body p1 p2 =
-    let check eq f = if not (eq (f p1) (f p2)) then error () in
-    check MutInd.equal (fun x -> x.proj_ind);
-    check (==) (fun x -> x.proj_npars);
-    check (==) (fun x -> x.proj_arg);
-    check (eq_constr) (fun x -> x.proj_type);
-    check (eq_constr) (fun x -> fst x.proj_eta);
-    check (eq_constr) (fun x -> snd x.proj_eta);
-    check (eq_constr) (fun x -> x.proj_body); true
-  in
   let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in
 
   let check_packet p1 p2 =
@@ -186,16 +175,19 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   (* we check that records and their field names are preserved. *)
   let record_equal x y =
     match x, y with
-    | None, None -> true
-    | Some None, Some None -> true
-    | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
-      Id.equal id1 id2 &&
-      Array.for_all2 Constant.UserOrd.equal p1 p2 &&
-      Array.for_all2 eq_projection_body pb1 pb2
+    | NotRecord, NotRecord -> true
+    | FakeRecord, FakeRecord -> true
+    | PrimRecord info1, PrimRecord info2 ->
+      let check (id1, p1, pb1) (id2, p2, pb2) =
+        (* we don't care about the id, the types are inferred from the inductive
+           (ie checked before now) *)
+        Array.for_all2 Label.equal p1 p2
+      in
+      Array.equal check info1 info2
     | _, _ -> false
   in
   check record_equal (fun mib -> mib.mind_record);
-  if mib1.mind_record != None then begin
+  if mib1.mind_record != NotRecord 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)
@@ -216,7 +208,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets
   in ()
 
-let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
+let check_constant env l info1 cb2 spec2 subst1 subst2 =
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
   let check_type env t1 t2 = check_conv conv_leq env t1 t2 in
@@ -280,7 +272,7 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
   let check_one_body  (l,spec2) =
       match spec2 with
 	| SFBconst cb2 ->
-	    check_constant  env mp1 l (get_obj mp1 map1 l)
+            check_constant env l (get_obj mp1 map1 l)
 	      cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
 	    check_inductive env mp1 l (get_obj mp1 map1 l)
diff --git a/checker/term.ml b/checker/term.ml
index 0236f786..d84491b3 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -20,15 +20,15 @@ open Cic
 (* Sorts. *)
 
 let family_of_sort = function
-  | Prop Null -> InProp
-  | Prop Pos -> InSet
+  | Prop -> InProp
+  | Set -> InSet
   | Type _ -> InType
 
 let family_equal = (==)
 
 let sort_of_univ u =
-  if Univ.is_type0m_univ u then Prop Null
-  else if Univ.is_type0_univ u then Prop Pos
+  if Univ.is_type0m_univ u then Prop
+  else if Univ.is_type0_univ u then Set
   else Type u
 
 (********************************************************************)
@@ -243,7 +243,7 @@ let map_rel_decl f = function
        LocalDef (n, body', typ')
 
 let map_rel_context f =
-  List.smartmap (map_rel_decl f)
+  List.Smart.map (map_rel_decl f)
 
 let extended_rel_list n hyps =
   let rec reln l p = function
@@ -356,15 +356,11 @@ let rec isArity c =
 (* alpha conversion : ignore print names and casts *)
 
 let compare_sorts s1 s2 = match s1, s2 with
-| Prop c1, Prop c2 ->
-  begin match c1, c2 with
-  | Pos, Pos | Null, Null -> true
-  | Pos, Null -> false
-  | Null, Pos -> false
-  end
+| Prop, Prop | Set, Set -> true
 | Type u1, Type u2 -> Univ.Universe.equal u1 u2
-| Prop _, Type _ -> false
-| Type _, Prop _ -> false
+| Prop, Set | Set, Prop -> false
+| (Prop | Set), Type _ -> false
+| Type _, (Prop | Set) -> false
 
 let eq_puniverses f (c1,u1) (c2,u2) =
   Univ.Instance.equal u1 u2 && f c1 c2
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 18f07dc0..e4c3f4ae 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -103,11 +103,11 @@ let judge_of_apply env (f,funj) argjv =
 let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
     (* Product rule (s,Prop,Prop) *)
-    | (_,       Prop Null)  -> rangsort
+    | _,       Prop  -> rangsort
     (* Product rule (Prop/Set,Set,Set) *)
-    | (Prop _,  Prop Pos) -> rangsort
+    | (Prop | Set),  Set -> rangsort
     (* Product rule (Type,Set,?) *)
-    | (Type u1, Prop Pos) ->
+    | Type u1, Set ->
         if engagement env = ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
@@ -115,11 +115,11 @@ let sort_of_product env domsort rangsort =
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Univ.sup u1 Univ.type0_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (Univ.sup Univ.type0_univ u2)
+    | Set,  Type u2  -> Type (Univ.sup Univ.type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Null, Type _)  -> rangsort
+    | Prop, Type _  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
-    | (Type u1, Type u2) -> Type (Univ.sup u1 u2)
+    | Type u1, Type u2 -> Type (Univ.sup u1 u2)
 
 (* Type of a type cast *)
 
@@ -158,7 +158,7 @@ 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: "^MutInd.to_string (fst ind))
+      failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
   in
   type_of_inductive_knowing_parameters env (specif,u) paramstyp
 
@@ -172,7 +172,7 @@ let judge_of_constructor env (c,u) =
   let specif =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
+      failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
   in
   type_of_constructor (c,u) specif
 
@@ -198,14 +198,13 @@ let judge_of_case env ci pj (c,cj) lfj =
 (* Projection. *)
 
 let judge_of_projection env p c ct =
-  let pb = lookup_projection p env in
+  let pty = 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(MutInd.equal pb.proj_ind (fst ind));
-    let ty = subst_instance_constr u pb.proj_type in
-      substl (c :: List.rev args) ty
+  let ty = subst_instance_constr u pty in
+  substl (c :: List.rev args) ty
 
 (* Fixpoints. *)
 
@@ -239,7 +238,7 @@ let type_fixpoint env lna lar lbody vdefj =
 let rec execute env cstr =
   match cstr with
     (* Atomic terms *)
-    | Sort (Prop _) -> judge_of_prop
+    | Sort (Prop | Set) -> judge_of_prop
 
     | Sort (Type u) -> judge_of_type u
 
diff --git a/checker/univ.ml b/checker/univ.ml
index 1619010c..a0511ad2 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -142,7 +142,13 @@ end
 
 (** Level sets and maps *)
 module LMap = HMap.Make (Level)
-module LSet = LMap.Set
+module LSet = struct
+  include LMap.Set
+
+  let pr s =
+    str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
+
+end
 
 type 'a universe_map = 'a LMap.t
 
@@ -301,7 +307,7 @@ struct
 
   let for_all = List.for_all
 
-  let smartmap = List.smartmap
+  let smart_map = List.Smart.map
 
 end
 
@@ -863,12 +869,12 @@ struct
   let is_empty x = Int.equal (Array.length x) 0
 
   let subst_fn fn t = 
-    let t' = CArray.smartmap fn t in
+    let t' = CArray.Smart.map fn t in
       if t' == t then t else t'
 
   let subst s t =
     let t' = 
-      CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
+      CArray.Smart.map (fun x -> try LMap.find x s with Not_found -> x) t
     in if t' == t then t else t'
 
   let pr =
@@ -904,11 +910,11 @@ let subst_instance_level s l =
   | _ -> l
 
 let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
+  Array.Smart.map (fun l -> subst_instance_level s l) i
 
 let subst_instance_universe s u =
   let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
+  let u' = Universe.smart_map f u in
     if u == u' then u
     else Universe.sort u'
 
@@ -1049,7 +1055,7 @@ let subst_univs_level_level subst l =
 
 let subst_univs_level_universe subst u =
   let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
-  let u' = Universe.smartmap f u in
+  let u' = Universe.smart_map f u in
     if u == u' then u
     else Universe.sort u'
 
@@ -1082,14 +1088,13 @@ let subst_univs_universe fn ul =
 
 let merge_context strict ctx g =
   let g = Array.fold_left
-   (* Be lenient, module typing reintroduces universes and 
-      constraints due to includes *)
-	    (fun g v -> try add_universe v strict g with AlreadyDeclared -> g)
+            (fun g v -> add_universe v strict g)
 	    g (UContext.instance ctx)
   in merge_constraints (UContext.constraints ctx) g
 
 let merge_context_set strict ctx g =
   let g = LSet.fold
+   (* Include and side effects still have double-declared universes *)
 	    (fun v g -> try add_universe v strict g with AlreadyDeclared -> g)
 	    (ContextSet.levels ctx) g
   in merge_constraints (ContextSet.constraints ctx) g
diff --git a/checker/univ.mli b/checker/univ.mli
index 473159c0..3b29b158 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -49,6 +49,7 @@ sig
   val make : Level.t -> t
   (** Create a universe representing the given level. *)
 
+  val pr : t -> Pp.t
 end
 
 type universe = Universe.t
@@ -138,7 +139,14 @@ val check_constraints : constraints -> universes -> bool
 
 (** Polymorphic maps from universe levels to 'a *)
 module LMap : CSig.MapS with type key = universe_level
-module LSet : CSig.SetS with type elt = universe_level
+module LSet :
+sig
+  include CSig.SetS with type elt = Level.t
+
+  val pr : t -> Pp.t
+  (** Pretty-printing *)
+end
+
 type 'a universe_map = 'a LMap.t
 
 (** {6 Substitution} *)
@@ -214,6 +222,8 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   val repr : t -> UContext.t
 
+  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+
 end
 
 type abstract_universe_context = AUContext.t
diff --git a/checker/values.ml b/checker/values.ml
index 1ac8d7ce..e1b5a949 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli
+MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli
 
 *)
 
@@ -91,7 +91,7 @@ let rec v_mp = Sum("module_path",0,
   [|[|v_dp|];
     [|v_uid|];
     [|v_mp;v_id|]|])
-let v_kn = v_tuple "kernel_name" [|Any;v_mp;v_dp;v_id;Int|]
+let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|]
 let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|]
 let v_ind = v_tuple "inductive" [|v_cst;Int|]
 let v_cons = v_tuple "constructor" [|v_ind;Int|]
@@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
 
-let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|]
+let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|]
 let v_sortfam = v_enum "sorts_family" 3
 
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
@@ -135,7 +135,9 @@ let v_caseinfo =
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 4
-let v_proj = v_tuple "projection" [|v_cst; v_bool|]
+
+let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|]
+let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
 
 let rec v_constr =
   Sum ("constr",0,[|
@@ -173,7 +175,7 @@ let v_section_ctxt = v_enum "emptylist" 1
 (** kernel/mod_subst *)
 
 let v_delta_hint =
-  v_sum "delta_hint" 0 [|[|Int; Opt v_constr|];[|v_kn|]|]
+  v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|]
 
 let v_resolver =
   v_tuple "delta_resolver"
@@ -223,14 +225,8 @@ let v_cst_def =
   v_sum "constant_def" 0
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
-let v_projbody =
-  v_tuple "projection_body"
-	  [|v_cst;Int;Int;v_constr;
-	    v_tuple "proj_eta" [|v_constr;v_constr|];
-	    v_constr|]
-
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|]
 
 let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
@@ -240,7 +236,6 @@ let v_cb = v_tuple "constant_body"
     v_constr;
     Any;
     v_const_univs;
-    Opt v_projbody;
     v_bool;
     v_typing_flags|]
 
@@ -277,8 +272,10 @@ let v_one_ind = v_tuple "one_inductive_body"
     Any|]
 
 let v_finite = v_enum "recursivity_kind" 3
-let v_mind_record = Annot ("mind_record", 
-			   Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
+
+let v_record_info =
+  v_sum "record_info" 2
+    [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
 
 let v_ind_pack_univs = 
   v_sum "abstract_inductive_universes" 0
@@ -286,7 +283,7 @@ let v_ind_pack_univs =
 
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
-    v_mind_record;
+    v_record_info;
     v_finite;
     Int;
     v_section_ctxt;