Option -type-in-type: added support in checker and making it contaminating

in vo files (this was not done yet in 24d0027f0 and 090fffa57b).

Reused field "engagement" to carry information about both
impredicativity of set and type in type.

For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?

26 files changed, 119 insertions, 101 deletions

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 05a2a1b99..d041f1b7e 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 0f7ed8df5..d5d9b9e3b 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 d75af7654..881d3ca79 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -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/environ.ml b/checker/environ.ml
index c0f366000..6dbc44d6b 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 *)
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 22fe7d8f1..f3b2dd839 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 *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 050c33e60..e1a6bc7c1 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/reduction.ml b/checker/reduction.ml
index 58f0f894f..8ddeea2a2 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -158,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
@@ -167,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)
@@ -261,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 810d6e0b6..dd9482313 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/typeops.ml b/checker/typeops.ml
index 9bc4b269b..21819992a 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 46b66adc4..e82ba1032 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -193,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|]
@@ -315,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 *)
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index c1c19a757..561c66b42 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,7 +14,10 @@ open Context
    declarations. This includes global constants/axioms, mutual
    inductive definitions, modules and module types *)
 
-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) } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a79abbb7e..30b28177c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,11 +46,14 @@ let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
 
-let type_in_type env = env.env_stratification.env_type_in_type
-
 let is_impredicative_set env = 
-  match engagement env with
-  | Some ImpredicativeSet -> true
+  match fst (engagement env) with
+  | ImpredicativeSet -> true
+  | _ -> false
+
+let type_in_type env =
+  match snd (engagement env) with
+  | TypeInType -> true
   | _ -> false
 
 let universes env = env.env_stratification.env_universes
@@ -191,11 +194,7 @@ let check_constraints c env =
 
 let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
-    { env.env_stratification with env_engagement = Some c } }
-
-let set_type_in_type env =
-  { env with env_stratification =
-    { env.env_stratification with env_type_in_type = true } }
+    { env.env_stratification with env_engagement = c } }
 
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ede356e69..4ad0327fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab
 val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
 
 
-val engagement    : env -> engagement option
+val engagement    : env -> engagement
 val is_impredicative_set : env -> bool
-
-val type_in_type  : env -> bool
+val type_in_type : env -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
@@ -215,8 +214,6 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
 
-val set_type_in_type : env -> env
-
 (** {6 Sets of referred section variables }
    [global_vars_set env c] returns the list of [id]'s occurring either
    directly as [Var id] in [c] or indirectly as a section variable
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64c..d22abff10 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -182,14 +182,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 31c0e83c8..9c79009db 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,7 +173,7 @@ let cumulate_arity_large_levels env sign =
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
-  is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+  is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
 
 (* Returns the list [x_1, ..., x_n] of levels contributing to template
    polymorphism. The elements x_k is None if the k-th parameter (starting
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 557ed3d7d..5f3f559a2 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -46,8 +46,7 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option;
-  env_type_in_type : bool
+  env_engagement : engagement
 }
 
 type val_kind =
@@ -95,8 +94,7 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = initial_universes;
-    env_engagement = None;
-    env_type_in_type = false};
+    env_engagement = (PredicativeSet,StratifiedType) };
   env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
   indirect_pterms = Opaqueproof.empty_opaquetab }
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 03ac41b45..0ce0bed23 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,8 +33,7 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option;
-  env_type_in_type : bool
+  env_engagement : engagement
 }
 
 type lazy_val
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d8473183a..907ad2a1d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -184,16 +184,20 @@ let set_engagement c senv =
 
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
-let check_engagement env c =
-  match Environ.engagement env, c with
-  | None, Some ImpredicativeSet ->
-    Errors.error "Needs option -impredicative-set."
-  | _ -> ()
-
-let set_type_in_type senv = 
-  { senv with
-    env = Environ.set_type_in_type senv.env;
-    type_in_type = true }
+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
 
 (** {6 Stm machinery } *)
 
@@ -734,7 +738,7 @@ type compiled_library = {
   comp_name : DirPath.t;
   comp_mod : module_body;
   comp_deps : library_info array;
-  comp_enga : engagement option;
+  comp_enga : engagement;
   comp_natsymbs : Nativecode.symbols
 }
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1e9cdbda0..2b4324b96 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -99,12 +99,9 @@ val add_constraints :
 (* (\** Generator of universes *\) *)
 (* val next_universe : int safe_transformer *)
 
-(** Setting the strongly constructive or classical logical engagement *)
+(** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
 
-(** Collapsing the type hierarchy *)
-val set_type_in_type : safe_transformer0
-
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> module_path safe_transformer
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 48dbacf1a..fe82d85d5 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,14 +252,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
diff --git a/library/global.ml b/library/global.ml
index 49fa2ef28..0419799b6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -84,7 +84,6 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c)
 let push_context c = globalize0 (Safe_typing.push_context c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
-let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 75a1ebee9..363bb5789 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,7 +27,6 @@ val named_context : unit -> Context.named_context
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
-val set_type_in_type : unit -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index b4b6b8aab..2432b8d29 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -150,14 +150,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (sup u1 type0_univ)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 77339aef4..04238da2b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -360,8 +360,7 @@ let make_conclusion_flexible evdref ty poly =
   else () 
 	
 let is_impredicative env u = 
-  u = Prop Null || 
-  (engagement env = Some Declarations.ImpredicativeSet && u = Prop Pos)
+  u = Prop Null || (is_impredicative_set env && u = Prop Pos)
 
 let interp_ind_arity env evdref ind =
   let c = intern_gen IsType env ind.ind_arity in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5b330cd25..5540dc0ff 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -112,14 +112,12 @@ let print_memory_stat () =
 
 let _ = at_exit print_memory_stat
 
-let engagement = ref None
-let set_engagement c = engagement := Some c
+let impredicative_set = ref Declarations.PredicativeSet
+let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet
+let type_in_type = ref Declarations.StratifiedType
+let set_type_in_type () = type_in_type := Declarations.TypeInType
 let engage () =
-  match !engagement with Some c -> Global.set_engagement c | None -> ()
-
-let type_in_type = ref false
-let set_type_in_type () = type_in_type := true
-let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
+  Global.set_engagement (!impredicative_set,!type_in_type)
 
 let set_batch_mode () = batch_mode := true
 
@@ -521,7 +519,7 @@ let parse_args arglist =
     |"-filteropts" -> filter_opts := true
     |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
     |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
-    |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+    |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
     |"-just-parsing" -> Vernac.just_parsing := true
     |"-m"|"--memory" -> memory_stat := true
@@ -605,7 +603,6 @@ let init arglist =
       Mltop.init_known_plugins ();
       set_vm_opt ();
       engage ();
-      set_hierarchy ();
       (* Be careful to set these variables after the inputstate *)
       Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
       Syntax_def.set_compat_notations (not !no_compat_ntn);
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 737b7fb59..15ad18d9c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -135,7 +135,7 @@ let typecheck_params_and_fields def id t ps nots fs =
     let ctx, aritysort = Reduction.dest_arity env0 arity in
       assert(List.is_empty ctx); (* Ensured by above analysis *)
       if Sorts.is_prop aritysort || 
-	(Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then
+	(Sorts.is_set aritysort && is_impredicative_set env0) then
 	evars
       else Evd.set_leq_sort env_ar evars (Type univ) aritysort
   in