Merge branch 'v8.5'

16 files changed, 152 insertions, 106 deletions

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 05a2a1b992..d041f1b7e1 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,11 +23,17 @@ let print_memory_stat () =
 
 let output_context = ref false
 
-let pr_engt = function
-    Some ImpredicativeSet ->
-      str "Theory: Set is impredicative"
-  | None ->
-      str "Theory: Set is predicative"
+let pr_engagement (impr_set,type_in_type) =
+  begin
+    match impr_set with
+    | ImpredicativeSet -> str "Theory: Set is impredicative"
+    | PredicativeSet -> str "Theory: Set is predicative"
+  end ++
+  begin
+    match type_in_type with
+    | StratifiedType -> str "Theory: Stratified type hierarchy"
+    | TypeInType -> str "Theory: Type is of type Type"
+  end
 
 let cst_filter f csts =
   Cmap_env.fold
@@ -54,7 +60,7 @@ let print_context env =
     ppnl(hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
-      str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
       fnl())); pp_flush()
   end
diff --git a/checker/checker.ml b/checker/checker.ml
index 0f7ed8df51..d5d9b9e3b8 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -138,10 +138,11 @@ let init_load_path () =
 
 let set_debug () = Flags.debug := true
 
-let engagement = ref None
-let set_engagement c = engagement := Some c
-let engage () =
-  match !engagement with Some c -> Safe_typing.set_engagement c | None -> ()
+let impredicative_set = ref Cic.PredicativeSet
+let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
+let type_in_type = ref Cic.StratifiedType
+let set_type_in_type () = type_in_type := Cic.TypeInType
+let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type)
 
 
 let admit_list = ref ([] : section_path list)
@@ -194,6 +195,7 @@ let print_usage_channel co command =
 \n  -silent                disable trace of constants being checked\
 \n\
 \n  -impredicative-set     set sort Set impredicative\
+\n  -type-in-type          collapse type hierarchy\
 \n\
 \n  -h, --help             print this list of options\
 \n"
@@ -319,7 +321,9 @@ let parse_args argv =
   let rec parse = function
     | [] -> ()
     | "-impredicative-set" :: rem ->
-      set_engagement Cic.ImpredicativeSet; parse rem
+      set_impredicative_set (); parse rem
+    | "-type-in-type" :: rem ->
+      set_type_in_type (); parse rem
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
diff --git a/checker/cic.mli b/checker/cic.mli
index e875e40f0a..881d3ca797 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -102,7 +102,7 @@ type constr =
   | Case      of case_info * constr * constr * constr array
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
-  | Proj      of constant * constr
+  | Proj      of projection * constr
 
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
@@ -165,7 +165,10 @@ type action
 
 (** Engagements *)
 
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -407,7 +410,7 @@ type compiled_library = {
   comp_name : compilation_unit_name;
   comp_mod : module_body;
   comp_deps : library_deps;
-  comp_enga : engagement option;
+  comp_enga : engagement;
   comp_natsymbs : nativecode_symb_array
 }
 
diff --git a/checker/closure.ml b/checker/closure.ml
index 356b683fa8..c6cc2185d3 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -276,7 +276,7 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
@@ -308,7 +308,7 @@ type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * projection
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -678,8 +678,9 @@ let eta_expand_ind_stack env ind m s (f, s') =
       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 (p, right) }) projs 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 *)
 
@@ -738,7 +739,7 @@ let rec knh info m stk =
     | FCast(t,_,_) -> knh info t stk
 
     | FProj (p,c) ->
-      if red_set info.i_flags (fCONST p) then
+      if red_set info.i_flags (fCONST (Projection.constant p)) then
         (let pb = lookup_projection p (info.i_env) in
 	   knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
 		       :: zupdate m stk))
diff --git a/checker/closure.mli b/checker/closure.mli
index e6b39250d6..376e9fef7d 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -95,7 +95,7 @@ type fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
@@ -117,7 +117,7 @@ type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * projection
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8d913475f9..36e6a7caba 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -206,14 +206,15 @@ let rec map_kn f f' c =
   let func = map_kn f f' in
     match c with
       | 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 
+      | Proj (p,t) -> 
+          let p' = 
+	    Projection.map (fun kn ->
+			    try fst (f' kn Univ.Instance.empty)
+			    with No_subst -> kn) p
 	  in
 	  let t' = func t in
-	    if kn' == kn && t' == t then c
-	    else Proj (kn', t')
+	    if p' == p && t' == t then c
+	    else Proj (p', t')
       | Ind ((kn,i),u) ->
 	  let kn' = f kn in
 	  if kn'==kn then c else Ind ((kn',i),u)
diff --git a/checker/environ.ml b/checker/environ.ml
index 710ebc7127..6dbc44d6b8 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -14,7 +14,7 @@ type globals = {
 
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : engagement option
+  env_engagement : engagement
 }
 
 type env = {
@@ -33,19 +33,28 @@ let empty_env = {
   env_rel_context = [];
   env_stratification =
   { env_universes = Univ.initial_universes;
-    env_engagement = None};
+    env_engagement = (PredicativeSet,StratifiedType)};
   env_imports = MPmap.empty }
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
 let rel_context env = env.env_rel_context
 
-let set_engagement c env =
-  match env.env_stratification.env_engagement with
-    | Some c' -> if c=c' then env else error "Incompatible engagement"
-    | None ->
-        { env with env_stratification =
-          { env.env_stratification with env_engagement = Some c } }
+let set_engagement (impr_set,type_in_type as c) env =
+  let expected_impr_set,expected_type_in_type =
+    env.env_stratification.env_engagement in
+  begin
+    match impr_set,expected_impr_set with
+    | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+    | _ -> ()
+  end;
+  begin
+    match type_in_type,expected_type_in_type with
+    | StratifiedType, TypeInType -> error "Incompatible engagement"
+    | _ -> ()
+  end;
+  { env with env_stratification =
+      { env.env_stratification with env_engagement = c } }
 
 (* Digests *)
 
@@ -147,8 +156,8 @@ let evaluable_constant cst env =
 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 
+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")
 
diff --git a/checker/environ.mli b/checker/environ.mli
index d3448b127f..f3b2dd839a 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -11,7 +11,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : engagement option;
+  env_engagement : engagement;
 }
 type env = {
   env_globals : globals;
@@ -22,7 +22,7 @@ type env = {
 val empty_env : env
 
 (* Engagement *)
-val engagement : env -> Cic.engagement option
+val engagement : env -> Cic.engagement
 val set_engagement : Cic.engagement -> env -> env
 
 (* Digests *)
@@ -51,7 +51,7 @@ 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
+val lookup_projection : projection -> env -> projection_body
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 050c33e603..e1a6bc7c1d 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
 (* Allowed eliminations *)
 
 let check_predicativity env s small level =
-  match s, engagement env with
+  match s, fst (engagement env) with
       Type u, _ ->
         (* let u' = fresh_local_univ () in *)
         (* let cst = *)
@@ -184,7 +184,7 @@ 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, Some ImpredicativeSet -> ()
+    | Prop Pos, ImpredicativeSet -> ()
     | Prop Pos, _ ->
         if not small then failwith "impredicative Set inductive type"
     | Prop Null,_ -> ()
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 59d1a645a5..21b80f323e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -103,13 +103,12 @@ let instantiate_params full t u args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
-  let t = mkArity (sign,dummy) in
+  let t = mkArity (subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let inst_ind = constructor_instantiate mind u mib in
-  (fun t ->
-    instantiate_params true (inst_ind t) u params mib.mind_params_ctxt)
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+  let inst_ind = constructor_instantiate mind u mib t in
+    instantiate_params true inst_ind u params mib.mind_params_ctxt
 
 (************************************************************************)
 (************************************************************************)
@@ -142,53 +141,60 @@ let sort_as_univ = function
 | Prop Null -> Univ.type0m_univ
 | Prop Pos -> 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 *)
+(* to [x]. *)
 let cons_subst u su subst =
-  Univ.LMap.add u su subst
-
-let actualize_decl_level env lev t =
-  let sign,s = dest_arity env t in
-  mkArity (sign,lev)
-
-let polymorphism_on_non_applied_parameters = false
+  try
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+  try
+    let su = Universe.make u in
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> subst
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env = function
-  | (_,Some _,_ as t)::sign, exp, args ->
-      let ctx,subst = make_subst env (sign, exp, args) in
-      t::ctx, subst
-  | d::sign, None::exp, args ->
-      let args = match args with _::args -> args | [] -> [] in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, subst
-  | d::sign, Some u::exp, a::args ->
-      (* We recover the level of the argument, but we don't change the *)
-      (* level in the corresponding type in the arity; this level in the *)
-      (* arity is a global level which, at typing time, will be enforce *)
-      (* to be greater than the level of the argument; this is probably *)
-      (* a useless extra constraint *)
-      let s = sort_as_univ (snd (dest_arity env a)) in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, cons_subst u s subst
-  | (na,None,t as d)::sign, Some u::exp, [] ->
-      (* No more argument here: we instantiate the type with a fresh level *)
-      (* which is first propagated to the corresponding premise in the arity *)
-      (* (actualize_decl_level), then to the conclusion of the arity (via *)
-      (* the substitution) *)
-      let ctx,subst = make_subst env (sign, exp, []) in
-	d::ctx, subst
-  | sign, [], _ ->
-      (* Uniform parameters are exhausted *)
-      sign,Univ.LMap.empty
-  | [], _, _ ->
-      assert false
-
+let rec make_subst env =
+  let rec make subst = function
+    | (_,Some _,_)::sign, exp, args ->
+        make subst (sign, exp, args)
+    | d::sign, None::exp, args ->
+        let args = match args with _::args -> args | [] -> [] in
+        make subst (sign, exp, args)
+    | d::sign, Some u::exp, a::args ->
+        (* We recover the level of the argument, but we don't change the *)
+        (* level in the corresponding type in the arity; this level in the *)
+        (* arity is a global level which, at typing time, will be enforce *)
+        (* to be greater than the level of the argument; this is probably *)
+        (* a useless extra constraint *)
+        let s = sort_as_univ (snd (dest_arity env a)) in
+        make (cons_subst u s subst) (sign, exp, args)
+    | (na,None,t)::sign, Some u::exp, [] ->
+        (* No more argument here: we add the remaining universes to the *)
+        (* substitution (when [u] is distinct from all other universes in the *)
+        (* template, it is identity substitution  otherwise (ie. when u is *)
+        (* already in the domain of the substitution) [remember_subst] will *)
+        (* update its image [x] by [sup x u] in order not to forget the *)
+        (* dependency in [u] that remains to be fullfilled. *)
+        make (remember_subst u subst) (sign, exp, [])
+    | sign, [], _ ->
+        (* Uniform parameters are exhausted *)
+        subst
+    | [], _, _ ->
+        assert false
+  in
+  make Univ.LMap.empty
 
 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 subst = make_subst env (ctx,ar.template_param_levels,args) in
   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 *)
diff --git a/checker/print.ml b/checker/print.ml
index 1cc48ff774..7624fd3257 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -100,7 +100,7 @@ let print_pure_constr csr =
         done
       in print_string"{"; print_fix (); print_string"}"
   | Proj (p, c) ->
-    print_string "Proj("; sp_con_display p; print_string ","; 
+    print_string "Proj("; sp_con_display (Projection.constant 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 28fdb130e8..8ddeea2a20 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.constant * lift
+  | Zlproj of Names.projection * 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
@@ -137,7 +137,9 @@ 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.eq_con_chk c1 c2) then 
+	       if not (Names.eq_con_chk
+		       (Names.Projection.constant c1)
+		       (Names.Projection.constant c2)) then 
 		raise NotConvertible
             | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
@@ -156,7 +158,7 @@ type conv_pb =
   | CONV
   | CUMUL
 
-let sort_cmp univ pb s0 s1 =
+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
@@ -165,7 +167,8 @@ let sort_cmp univ pb s0 s1 =
             CUMUL -> ()
           | _ -> raise NotConvertible)
     | (Type u1, Type u2) ->
-        if not
+        if snd (engagement env) == StratifiedType
+          && not
 	  (match pb with
             | CONV -> Univ.check_eq univ u1 u2
 	    | CUMUL -> Univ.check_leq univ u1 u2)
@@ -259,7 +262,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 	(match a1, a2 with
 	   | (Sort s1, Sort s2) ->
 	       assert (is_empty_stack v1 && is_empty_stack v2);
-	       sort_cmp univ cv_pb s1 s2
+	       sort_cmp (infos_env infos) univ cv_pb s1 s2
 	   | (Meta n, Meta m) ->
                if n=m
 	       then convert_stacks univ infos lft1 lft2 v1 v2
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 810d6e0b65..dd94823135 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -32,13 +32,21 @@ let full_add_module dp mb univs digest =
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
-(* Check that the engagement expected by a library matches the initial one *)
-let check_engagement env c =
-  match engagement env, c with
-    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
-    | _, None -> ()
-    | _, Some ImpredicativeSet ->
-        error "Needs option -impredicative-set"
+(* Check that the engagement expected by a library extends the initial one *)
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+  let impredicative_set,type_in_type = Environ.engagement env in
+  begin
+    match impredicative_set, expected_impredicative_set with
+    | PredicativeSet, ImpredicativeSet ->
+        Errors.error "Needs option -impredicative-set."
+    | _ -> ()
+  end;
+  begin
+    match type_in_type, expected_type_in_type with
+    | StratifiedType, TypeInType ->
+        Errors.error "Needs option -type-in-type."
+    | _ -> ()
+  end
 
 (* Libraries = Compiled modules *)
 
diff --git a/checker/term.ml b/checker/term.ml
index 93540276b7..430be49519 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -392,7 +392,7 @@ let compare_constr f t1 t2 =
       Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
       Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2
+  | Proj (p1,c1), Proj(p2,c2) -> Projection.equal p1 p2 && f c1 c2
   | _ -> false
 
 let rec eq_constr m n =
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 9bc4b269b8..21819992a9 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if engagement env = Some ImpredicativeSet then
+        if fst (engagement env) = ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
         else
diff --git a/checker/values.ml b/checker/values.ml
index b2d74821d4..45220bd051 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
+MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli
 
 *)
 
@@ -126,6 +126,7 @@ 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 rec v_constr =
   Sum ("constr",0,[|
@@ -145,7 +146,7 @@ let rec v_constr =
     [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
-    [|v_cst;v_constr|] (* Proj *)
+    [|v_proj;v_constr|] (* Proj *)
   |])
 
 and v_prec = Tuple ("prec_declaration",
@@ -192,7 +193,9 @@ let v_lazy_constr =
 
 (** kernel/declarations *)
 
-let v_engagement = v_enum "eng" 1
+let v_impredicative_set = v_enum "impr-set" 2
+let v_type_in_type = v_enum "type-in-type" 2
+let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|]
 
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -205,8 +208,10 @@ let v_cst_def =
     [|[|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|]
+  v_tuple "projection_body"
+	  [|v_cst;Int;Int;v_constr;
+	    v_tuple "proj_eta" [|v_constr;v_constr|];
+	    v_constr|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
@@ -312,7 +317,7 @@ and v_modtype =
 let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
 let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_compiled_lib =
-  v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
+  v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
 
 (** Library objects *)