Merge PR# 169: Local type-in-type flag.

50 files changed, 260 insertions, 264 deletions

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index a63705adc..f196746a5 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,16 +23,11 @@ let print_memory_stat () =
 
 let output_context = ref false
 
-let pr_engagement (impr_set,type_in_type) =
+let pr_engagement impr_set =
   begin
     match impr_set with
     | ImpredicativeSet -> str "Theory: Set is impredicative"
     | PredicativeSet -> str "Theory: Set is predicative"
-  end ++ fnl() ++
-  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 =
diff --git a/checker/checker.ml b/checker/checker.ml
index 9d76fb09e..2c872f272 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -140,9 +140,7 @@ let set_debug () = Flags.debug := true
 
 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 engage () = Safe_typing.set_engagement (!impredicative_set)
 
 
 let admit_list = ref ([] : section_path list)
@@ -192,7 +190,6 @@ 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"
@@ -313,8 +310,6 @@ let parse_args argv =
     | [] -> ()
     | "-impredicative-set" :: 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 469cf8d4c..364558755 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -167,9 +167,8 @@ type action
 (** Engagements *)
 
 type set_predicativity = ImpredicativeSet | PredicativeSet
-type type_hierarchy = TypeInType | StratifiedType
 
-type engagement = set_predicativity * type_hierarchy
+type engagement = set_predicativity
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -219,6 +218,7 @@ type constant_universes = Univ.universe_context
 type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
+  check_universes : bool; (** If [false] universe constraints are not checked *)
 }
 
 type constant_body = {
@@ -327,11 +327,7 @@ type mutual_inductive_body = {
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
-    mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker.  *)
-
-(** {8 Data for native compilation } *)
-
-    mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
+    mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
   }
 
 (** {6 Module declarations } *)
diff --git a/checker/environ.ml b/checker/environ.ml
index 9352f71ef..881284eda 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -33,26 +33,21 @@ let empty_env = {
   env_rel_context = [];
   env_stratification =
   { env_universes = Univ.initial_universes;
-    env_engagement = (PredicativeSet,StratifiedType)};
+    env_engagement = PredicativeSet };
   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 (impr_set,type_in_type as c) env =
-  let expected_impr_set,expected_type_in_type =
+let set_engagement (impr_set as c) env =
+  let expected_impr_set =
     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 } }
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index a667bb8a3..29b16392b 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, fst (engagement env) with
+  match s, engagement env with
       Type u, _ ->
         (* let u' = fresh_local_univ () in *)
         (* let cst = *)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index f1aa5d919..b280df54a 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -167,8 +167,9 @@ let sort_cmp env univ pb s0 s1 =
             CUMUL -> ()
           | _ -> raise NotConvertible)
     | (Type u1, Type u2) ->
-        if snd (engagement env) == StratifiedType
-          && not
+        (** 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)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 1071e2f93..e644febe4 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -35,20 +35,15 @@ let full_add_module dp mb univs digest =
   genv := add_digest env dp digest
 
 (* 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
+let check_engagement env expected_impredicative_set =
+  let impredicative_set = 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 da9842a8d..0c7e538be 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 fst (engagement env) = ImpredicativeSet then
+        if 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 dd29f6fbe..c175aed68 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 7d7963269852d32324e10aa77beb938d  checker/cic.mli
+MD5 6466d8cc443b5896cb905776df0cc49e  checker/cic.mli
 
 *)
 
@@ -194,8 +194,7 @@ let v_lazy_constr =
 (** kernel/declarations *)
 
 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_engagement = v_impredicative_set
 
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -214,7 +213,7 @@ let v_projbody =
 	    v_constr|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
@@ -275,7 +274,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_bool;
     v_context;
     Opt v_bool;
-    v_bool|]
+    v_typing_flags|]
 
 let v_with =
   Sum ("with_declaration_body",0,
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 8b42a90e4..f89773fcc 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,9 +14,8 @@ open Term
    inductive definitions, modules and module types *)
 
 type set_predicativity = ImpredicativeSet | PredicativeSet
-type type_hierarchy = TypeInType | StratifiedType
 
-type engagement = set_predicativity * type_hierarchy
+type engagement = set_predicativity
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -73,6 +72,7 @@ type constant_universes = Univ.universe_context
 type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
+  check_universes : bool; (** If [false] universe constraints are not checked *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
@@ -190,8 +190,8 @@ type mutual_inductive_body = {
     mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
-  
-    mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker.  *)
+
+    mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
 }
 
 (** {6 Module declarations } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 28f7e69cd..211e5e062 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -16,6 +16,7 @@ open Context.Rel.Declaration
 
 let safe_flags = {
   check_guarded = true;
+  check_universes = true;
 }
 
 (** {6 Arities } *)
@@ -260,7 +261,7 @@ let subst_mind_body sub mib =
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
-    mind_checked_positive = mib.mind_checked_positive;
+    mind_typing_flags = mib.mind_typing_flags;
   }
 
 let inductive_instance mib =
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 8b29e3abd..df2c4653f 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -52,8 +52,6 @@ type mutual_inductive_entry = {
   mind_entry_polymorphic : bool; 
   mind_entry_universes : Univ.universe_context;
   mind_entry_private : bool option;
-  mind_entry_check_positivity : bool;
-  (** [false] if positivity is to be assumed. *)
 }
 
 (** {6 Constants (Definition/Axiom) } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d8493d9ba..9fb3bf79f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -45,16 +45,15 @@ let empty_named_context_val = empty_named_context_val
 let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
+let typing_flags env = env.env_typing_flags
 
 let is_impredicative_set env = 
-  match fst (engagement env) with
+  match engagement env with
   | ImpredicativeSet -> true
   | _ -> false
 
-let type_in_type env =
-  match snd (engagement env) with
-  | TypeInType -> true
-  | _ -> false
+let type_in_type env = not (typing_flags env).check_universes
+let deactivated_guard env = not (typing_flags env).check_guarded
 
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
@@ -211,6 +210,9 @@ let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
     { env.env_stratification with env_engagement = c } }
 
+let set_typing_flags c env = (* Unsafe *)
+  { env with env_typing_flags = c }
+
 (* Global constants *)
 
 let lookup_constant = lookup_constant
@@ -328,6 +330,9 @@ let polymorphic_pconstant (cst,u) env =
   if Univ.Instance.is_empty u then false
   else polymorphic_constant cst env
 
+let type_in_type_constant cst env =
+  not (lookup_constant cst env).const_typing_flags.check_universes
+
 let template_polymorphic_constant cst env =
   match (lookup_constant cst env).const_type with 
   | TemplateArity _ -> true
@@ -357,6 +362,9 @@ let polymorphic_pind (ind,u) env =
   if Univ.Instance.is_empty u then false
   else polymorphic_ind ind env
 
+let type_in_type_ind (mind,i) env =
+  not (lookup_mind mind env).mind_typing_flags.check_universes
+
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with 
   | TemplateArity _ -> true
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 520389954..b5e576435 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,8 +50,10 @@ val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
 
 
 val engagement    : env -> engagement
+val typing_flags    : env -> typing_flags
 val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
+val deactivated_guard : env -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
@@ -136,6 +138,7 @@ val evaluable_constant : constant -> env -> bool
 (** New-style polymorphism *)
 val polymorphic_constant  : constant -> env -> bool
 val polymorphic_pconstant : pconstant -> env -> bool
+val type_in_type_constant : constant -> env -> bool
 
 (** Old-style polymorphism *)
 val template_polymorphic_constant  : constant -> env -> bool
@@ -183,6 +186,7 @@ val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 (** New-style polymorphism *)
 val polymorphic_ind  : inductive -> env -> bool
 val polymorphic_pind : pinductive -> env -> bool
+val type_in_type_ind : inductive -> env -> bool
 
 (** Old-style polymorphism *)
 val template_polymorphic_ind : inductive -> env -> bool
@@ -212,6 +216,7 @@ val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
+val set_typing_flags : typing_flags -> env -> env
 
 (** {6 Sets of referred section variables }
    [global_vars_set env c] returns the list of [id]'s occurring either
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 35c162cf3..c2c8ee242 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -327,7 +327,7 @@ let type_fixpoint env lna lar vdef vdeft =
     (* ATTENTION : faudra faire le typage du contexte des Const,
     Ind et Constructsi un jour cela devient des constructions
     arbitraires et non plus des variables *)
-let rec execute ~flags env cstr =
+let rec execute env cstr =
   let open Context.Rel.Declaration in
   match kind_of_term cstr with
     (* Atomic terms *)
@@ -347,12 +347,12 @@ let rec execute ~flags env cstr =
       judge_of_constant env c
 	
     | Proj (p, c) ->
-        let ct = execute ~flags env c in
+        let ct = execute env c in
           judge_of_projection env p c ct
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-        let argst = execute_array ~flags env args in
+        let argst = execute_array env args in
 	let ft =
 	  match kind_of_term f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
@@ -365,7 +365,7 @@ let rec execute ~flags env cstr =
 	      judge_of_constant_knowing_parameters env cst args
 	  | _ ->
 	    (* Full or no sort-polymorphism *)
-            execute ~flags env f
+            execute env f
 	in
 
 	  judge_of_apply env f ft args argst
@@ -373,25 +373,25 @@ let rec execute ~flags env cstr =
     | Lambda (name,c1,c2) ->
       let _ = execute_is_type env c1 in
       let env1 = push_rel (LocalAssum (name,c1)) env in
-      let c2t = execute ~flags env1 c2 in
+      let c2t = execute env1 c2 in
         judge_of_abstraction env name c1 c2t
 
     | Prod (name,c1,c2) ->
-      let vars = execute_is_type ~flags env c1 in
+      let vars = execute_is_type env c1 in
       let env1 = push_rel (LocalAssum (name,c1)) env in
-      let vars' = execute_is_type ~flags env1 c2 in
+      let vars' = execute_is_type env1 c2 in
 	judge_of_product env name vars vars'
 
     | LetIn (name,c1,c2,c3) ->
-      let c1t = execute ~flags env c1 in
+      let c1t = execute env c1 in
       let _c2s = execute_is_type env c2 in
       let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in
       let env1 = push_rel (LocalDef (name,c1,c2)) env in
-      let c3t = execute ~flags env1 c3 in
+      let c3t = execute env1 c3 in
 	subst1 c1 c3t
 
     | Cast (c,k,t) ->
-      let ct = execute ~flags env c in
+      let ct = execute env c in
       let _ts = execute_type env t in
       let _ = judge_of_cast env c ct k t in
 	t
@@ -404,20 +404,20 @@ let rec execute ~flags env cstr =
       judge_of_constructor env c
 
     | Case (ci,p,c,lf) ->
-        let ct = execute ~flags env c in
-        let pt = execute ~flags env p in
-        let lft = execute_array ~flags env lf in
+        let ct = execute env c in
+        let pt = execute env p in
+        let lft = execute_array env lf in
           judge_of_case env ci p pt c ct lf lft
 
     | Fix ((vn,i as vni),recdef) ->
-      let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
+      let (fix_ty,recdef') = execute_recdef env recdef i in
       let fix = (vni,recdef') in
-        check_fix env ~flags fix; fix_ty
+        check_fix env fix; fix_ty
 	  
     | CoFix (i,recdef) ->
-      let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
+      let (fix_ty,recdef') = execute_recdef env recdef i in
       let cofix = (i,recdef') in
-        check_cofix env ~flags cofix; fix_ty
+        check_cofix env cofix; fix_ty
 	  
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
@@ -426,41 +426,38 @@ let rec execute ~flags env cstr =
     | Evar _ ->
 	anomaly (Pp.str "the kernel does not support existential variables")
 
-and execute_is_type ~flags env constr =
-  let t = execute ~flags env constr in
+and execute_is_type env constr =
+  let t = execute env constr in
     check_type env constr t
 
-and execute_type ~flags env constr =
-  let t = execute ~flags env constr in
+and execute_type env constr =
+  let t = execute env constr in
     type_judgment env constr t
 
-and execute_recdef ~flags env (names,lar,vdef) i =
-  let lart = execute_array ~flags env lar in
+and execute_recdef env (names,lar,vdef) i =
+  let lart = execute_array env lar in
   let lara = Array.map2 (assumption_of_judgment env) lar lart in
   let env1 = push_rec_types (names,lara,vdef) env in
-  let vdeft = execute_array ~flags env1 vdef in
+  let vdeft = execute_array env1 vdef in
   let () = type_fixpoint env1 names lara vdef vdeft in
     (lara.(i),(names,lara,vdef))
 
-and execute_array ~flags env = Array.map (execute ~flags env)
+and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
-let infer ~flags env constr =
-  let t = execute ~flags env constr in
+let infer env constr =
+  let t = execute env constr in
     make_judge constr t
 
 let infer = 
   if Flags.profile then
     let infer_key = Profile.declare_profile "Fast_infer" in
-      Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c)
-  else (fun a b c -> infer ~flags:a b c)
+      Profile.profile2 infer_key (fun b c -> infer b c)
+  else (fun b c -> infer b c)
 
-(* Restores the labels of [infer] lost to profiling. *)
-let infer ~flags env t = infer flags env t
+let infer_type env constr =
+  execute_type env constr
 
-let infer_type ~flags env constr =
-  execute_type ~flags env constr
-
-let infer_v ~flags env cv =
-  let jv = execute_array ~flags env cv in
+let infer_v env cv =
+  let jv = execute_array env cv in
     make_judgev cv jv
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 45a603038..41cff607e 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -19,6 +19,6 @@ open Declarations
  *)
 
 
-val infer      : flags:typing_flags -> env -> constr       -> unsafe_judgment
-val infer_v    : flags:typing_flags -> env -> constr array -> unsafe_judgment array
-val infer_type : flags:typing_flags -> env -> types        -> unsafe_type_judgment
+val infer      : env -> constr       -> unsafe_judgment
+val infer_v    : env -> constr array -> unsafe_judgment array
+val infer_type : env -> types        -> unsafe_type_judgment
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b74788d21..b6942e133 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -816,7 +816,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
 
-let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs is_checked =
+let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env inds in
@@ -922,7 +922,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
       mind_polymorphic = p;
       mind_universes = ctx;
       mind_private = prv;
-      mind_checked_positive = is_checked;
+      mind_typing_flags = Environ.typing_flags env;
     }
 
 (************************************************************************)
@@ -931,11 +931,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in
-  let chkpos = mie.mind_entry_check_positivity in
   (* Then check positivity conditions *)
+  let chkpos = (Environ.typing_flags env).check_guarded in
   let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
       env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
-      inds nmr recargs chkpos
+      inds nmr recargs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 24bdaa5c4..8e26370ec 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1067,7 +1067,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   (Array.map fst rv, Array.map snd rv)
 
 
-let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) =
+let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
+  let flags = Environ.typing_flags env in
   if flags.check_guarded then
     let (minds, rdef) = inductive_of_mutfix env fix in
     let get_tree (kn,i) =
@@ -1195,7 +1196,8 @@ let check_one_cofix env nbfix def deftype =
 (* The  function which checks that the whole block of definitions
    satisfies the guarded condition *)
 
-let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) =
+let check_cofix env (bodynum,(names,types,bodies as recdef)) =
+  let flags = Environ.typing_flags env in
   if flags.check_guarded then
     let nbfix = Array.length bodies in
     for i = 0 to nbfix-1 do
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 25a557472..521ee3c7b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -97,8 +97,8 @@ val check_case_info : env -> pinductive -> case_info -> unit
 
 (** When [chk] is false, the guard condition is not actually
     checked. *)
-val check_fix : env -> flags:typing_flags -> fixpoint -> unit
-val check_cofix : env -> flags:typing_flags -> cofixpoint -> unit
+val check_fix : env -> fixpoint -> unit
+val check_cofix : env -> cofixpoint -> unit
 
 (** {6 Support for sort-polymorphic inductive types } *)
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index c30789641..5afefeebd 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -71,6 +71,7 @@ type env = {
   env_rel_val       : lazy_val list;
   env_nb_rel        : int;
   env_stratification : stratification;
+  env_typing_flags  : typing_flags;
   env_conv_oracle   : Conv_oracle.oracle;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
@@ -93,7 +94,8 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = UGraph.initial_universes;
-    env_engagement = (PredicativeSet,StratifiedType) };
+    env_engagement = PredicativeSet };
+  env_typing_flags = Declareops.safe_flags;
   env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
   indirect_pterms = Opaqueproof.empty_opaquetab }
@@ -138,6 +140,7 @@ let push_named d env =
     env_rel_val = env.env_rel_val;
     env_nb_rel = env.env_nb_rel;
     env_stratification = env.env_stratification;
+    env_typing_flags = env.env_typing_flags;
     env_conv_oracle = env.env_conv_oracle;
     retroknowledge = env.retroknowledge;
     indirect_pterms = env.indirect_pterms;
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 353c46112..e551d22c8 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -50,6 +50,7 @@ type env = {
     env_rel_val       : lazy_val list;
     env_nb_rel        : int;
     env_stratification : stratification;
+    env_typing_flags  : typing_flags;
     env_conv_oracle   : Conv_oracle.oracle;
     retroknowledge : Retroknowledge.retroknowledge;
     indirect_pterms : Opaqueproof.opaquetab;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 72d6ee518..fc6155930 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -180,21 +180,18 @@ let set_engagement c senv =
     env = Environ.set_engagement c senv.env;
     engagement = Some c }
 
+let set_typing_flags c senv =
+  { senv with env = Environ.set_typing_flags c senv.env }
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
-let check_engagement env (expected_impredicative_set,expected_type_in_type) =
-  let impredicative_set,type_in_type = Environ.engagement env in
+let check_engagement env expected_impredicative_set =
+  let impredicative_set = 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 } *)
@@ -373,8 +370,8 @@ let safe_push_named d env =
   Environ.push_named d env
 
 
-let push_named_def ~flags (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def ~flags senv.revstruct senv.env id de in
+let push_named_def (id,de) senv =
+  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
   let poly = de.Entries.const_entry_polymorphic in
   let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
@@ -388,9 +385,9 @@ let push_named_def ~flags (id,de) senv =
   let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
     univs, {senv' with env=env''}
 
-let push_named_assum ~flags ((id,t,poly),ctx) senv =
+let push_named_assum ((id,t,poly),ctx) senv =
   let senv' = push_context_set poly ctx senv in
-  let t = Term_typing.translate_local_assum ~flags senv'.env t in
+  let t = Term_typing.translate_local_assum senv'.env t in
   let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in
     {senv' with env=env''}
 
@@ -479,7 +476,7 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags
+  | ConstantEntry of bool * private_constants Entries.constant_entry
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
@@ -512,10 +509,10 @@ let add_constant dir l decl senv =
   let no_section = DirPath.is_empty dir in
   let seff_to_export, decl =
     match decl with
-    | ConstantEntry (true, ce, flags) ->
+    | ConstantEntry (true, ce) ->
         let exports, ce =
-          Term_typing.export_side_effects ~flags senv.revstruct senv.env ce in
-        exports, ConstantEntry (false, ce, flags)
+          Term_typing.export_side_effects senv.revstruct senv.env ce in
+        exports, ConstantEntry (false, ce)
     | _ -> [], decl
   in
   let senv =
@@ -524,8 +521,8 @@ let add_constant dir l decl senv =
   let senv =
     let cb = 
       match decl with
-      | ConstantEntry (export_seff,ce,flags) ->
-        Term_typing.translate_constant ~flags senv.revstruct senv.env kn ce
+      | ConstantEntry (export_seff,ce) ->
+        Term_typing.translate_constant senv.revstruct senv.env kn ce
       | GlobalRecipe r ->
         let cb = Term_typing.translate_recipe senv.env kn r in
         if no_section then Declareops.hcons_const_body cb else cb in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b614a368c..15ebc7d88 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -77,21 +77,19 @@ val is_joined_environment : safe_environment -> bool
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum :
-  flags:Declarations.typing_flags ->
   (Id.t * Term.types * bool (* polymorphic *))
     Univ.in_universe_context_set -> safe_transformer0
 
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
 val push_named_def :
-  flags:Declarations.typing_flags ->
   Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
 type global_declaration =
                   (* bool: export private constants *)
-  | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags
+  | ConstantEntry of bool * private_constants Entries.constant_entry
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
@@ -134,6 +132,7 @@ val add_constraints :
 
 (** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
+val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 
 (** {6 Interactive module functions } *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f0c116d27..be84cae6d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,18 +22,18 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let constrain_type ~flags env j poly subst = function
+let constrain_type env j poly subst = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
       make_polymorphic_if_constant_for_ind env j
     else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
   | `Some t ->
-      let tj = infer_type ~flags env t in
+      let tj = infer_type env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
   | `SomeWJ (t, tj) ->
-      let tj = infer_type ~flags env t in
+      let tj = infer_type env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
@@ -171,11 +171,11 @@ let feedback_completion_typecheck =
   Option.iter (fun state_id ->
       feedback ~id:(State state_id) Feedback.Complete)
 
-let infer_declaration ~flags ~trust env kn dcl =
+let infer_declaration ~trust env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context ~strict:(not poly) uctx env in
-      let j = infer ~flags env t in
+      let j = infer env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
       let c = Typeops.assumption_of_judgment env j in
@@ -196,7 +196,7 @@ let infer_declaration ~flags ~trust env kn dcl =
 	  let env' = push_context_set uctx env in
           let j =
             let body,env',ectx = skip_trusted_seff valid_signatures body env' in
-            let j = infer ~flags env' body in
+            let j = infer env' body in
             unzip ectx j in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
@@ -220,8 +220,8 @@ let infer_declaration ~flags ~trust env kn dcl =
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
       let usubst, univs =
 	Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in      
-      let j = infer ~flags env body in
-      let typ = constrain_type ~flags env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+      let j = infer env body in
+      let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
 	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
@@ -268,7 +268,7 @@ let record_aux env s_ty s_bo suggested_expr =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
   let open Context.Named.Declaration in
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
@@ -353,7 +353,7 @@ let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_cod
 	    const_polymorphic = poly;
 	    const_universes = univs;
 	    const_inline_code = inline_code;
-	    const_typing_flags = flags;
+	    const_typing_flags = Environ.typing_flags env;
 	    }
 	in
 	let env = add_constant kn cb env in
@@ -368,13 +368,13 @@ let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_cod
     const_polymorphic = poly;
     const_universes = univs;
     const_inline_code = inline_code;
-    const_typing_flags = flags }
+    const_typing_flags = Environ.typing_flags env }
 
 (*s Global and local constant declaration. *)
 
-let translate_constant ~flags mb env kn ce =
-  build_constant_declaration ~flags kn env
-    (infer_declaration ~flags ~trust:mb env (Some kn) ce)
+let translate_constant mb env kn ce =
+  build_constant_declaration kn env
+    (infer_declaration ~trust:mb env (Some kn) ce)
 
 let constant_entry_of_side_effect cb u =
   let pt =
@@ -409,7 +409,7 @@ type side_effect_role =
 type exported_side_effect = 
   constant * constant_body * side_effects constant_entry * side_effect_role
 
-let export_side_effects ~flags mb env ce =
+let export_side_effects mb env ce =
   match ce with
   | ParameterEntry _ | ProjectionEntry _ -> [], ce
   | DefinitionEntry c ->
@@ -450,7 +450,7 @@ let export_side_effects ~flags mb env ce =
            let env, cbs =
              List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
                let ce = constant_entry_of_side_effect ocb u in
-               let cb = translate_constant ~flags mb env kn ce in
+               let cb = translate_constant mb env kn ce in
                (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) 
              (env,[]) cbs in
            translate_seff sl rest (cbs @ acc) env
@@ -465,17 +465,17 @@ let export_side_effects ~flags mb env ce =
        translate_seff trusted seff [] env
 ;;
 
-let translate_local_assum ~flags env t =
-  let j = infer ~flags env t in
+let translate_local_assum env t =
+  let j = infer env t in
   let t = Typeops.assumption_of_judgment env j in
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration ~flags:Declareops.safe_flags kn env (Cooking.cook_constant env r)
+  build_constant_declaration kn env (Cooking.cook_constant env r)
 
-let translate_local_def ~flags mb env id centry =
+let translate_local_def mb env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-    infer_declaration ~flags ~trust:mb env None (DefinitionEntry centry) in
+    infer_declaration ~trust:mb env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
     match def with
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index b635f2d31..fcd95576c 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,10 +12,10 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : flags:typing_flags -> structure_body -> env -> Id.t -> side_effects definition_entry ->
+val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
   constant_def * types * constant_universes
 
-val translate_local_assum : flags:typing_flags -> env -> types -> types
+val translate_local_assum : env -> types -> types
 
 val mk_pure_proof : constr -> side_effects proof_output
 
@@ -32,7 +32,7 @@ val inline_entry_side_effects :
 val uniq_seff : side_effects -> side_effects
 
 val translate_constant :
-  flags:typing_flags -> structure_body -> env -> constant -> side_effects constant_entry ->
+  structure_body -> env -> constant -> side_effects constant_entry ->
     constant_body
 
 type side_effect_role =
@@ -47,7 +47,7 @@ type exported_side_effect =
  * be pushed in the safe_env by safe typing.  The main constant entry
  * needs to be translated as usual after this step. *)
 val export_side_effects :
-  flags:typing_flags -> structure_body -> env -> side_effects constant_entry ->
+  structure_body -> env -> side_effects constant_entry ->
     exported_side_effect list * side_effects constant_entry
 
 val constant_entry_of_side_effect :
@@ -60,11 +60,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : flags:typing_flags -> trust:structure_body -> env -> constant option -> 
+val infer_declaration : trust:structure_body -> env -> constant option -> 
   side_effects constant_entry -> Cooking.result
 
 val build_constant_declaration :
-  flags:typing_flags -> constant -> env -> Cooking.result -> constant_body
+  constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
   (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9b9792ce8..0ea68e2bc 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -500,13 +500,13 @@ let rec execute env cstr =
     | Fix ((vn,i as vni),recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let fix = (vni,recdef') in
-        check_fix ~flags:Declareops.safe_flags env fix;
+        check_fix env fix;
 	make_judge (mkFix fix) fix_ty
 	  
     | CoFix (i,recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let cofix = (i,recdef') in
-        check_cofix ~flags:Declareops.safe_flags env cofix;
+        check_cofix env cofix;
 	(make_judge (mkCoFix cofix) fix_ty)
 	  
     (* Partial proofs: unsupported by the kernel *)
diff --git a/library/declare.ml b/library/declare.ml
index 335263f8f..f809e9742 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -58,11 +58,11 @@ let cache_variable ((sp,_),o) =
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ~flags:Declareops.safe_flags ((id,ty,poly),ctx) in
+      let () = Global.push_named_assum ((id,ty,poly),ctx) in
       let impl = if impl then Implicit else Explicit in
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let univs = Global.push_named_def ~flags:Declareops.safe_flags (id,de) in
+      let univs = Global.push_named_def (id,de) in
       Explicit, de.const_entry_opaque,
       de.const_entry_polymorphic, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
@@ -180,7 +180,7 @@ let discharge_constant ((sp, kn), obj) =
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
   ConstantEntry
-    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), Declareops.safe_flags)
+    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -205,7 +205,7 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
 let declare_scheme = ref (fun _ _ -> assert false)
 let set_declare_scheme f = declare_scheme := f
 
-let declare_constant_common ~flags id cst =
+let declare_constant_common id cst =
   let update_tables c =
 (*  Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
     declare_constant_implicits c;
@@ -216,7 +216,7 @@ let declare_constant_common ~flags id cst =
   List.iter (fun (c,ce,role) ->
       (* handling of private_constants just exported *)
       let o = inConstant {
-        cst_decl = ConstantEntry (false, ce, flags);
+        cst_decl = ConstantEntry (false, ce);
         cst_hyps = [] ;
         cst_kind = IsProof Theorem;
         cst_locl = false;
@@ -246,7 +246,7 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let export = (* We deal with side effects *)
     match cd with
     | DefinitionEntry de when
@@ -259,24 +259,24 @@ let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualR
     | _ -> false
   in
   let cst = {
-    cst_decl = ConstantEntry (export,cd,flags);
+    cst_decl = ConstantEntry (export,cd);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
     cst_exported = [];
     cst_was_seff = false;
   } in
-  let kn = declare_constant_common id cst ~flags in
+  let kn = declare_constant_common id cst in
   let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
   kn
 
-let declare_definition ?flags ?(internal=UserIndividualRequest)
+let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
   let cb =
     definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
-    declare_constant ?flags ~internal ~local id
+    declare_constant ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of inductive blocks *)
@@ -354,7 +354,7 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_polymorphic = false;
   mind_entry_universes = Univ.UContext.empty;
   mind_entry_private = None;
-  mind_entry_check_positivity = true; })
+})
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
@@ -374,7 +374,7 @@ let declare_projections mind =
       Array.iteri (fun i kn ->
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
-	let kn' = declare_constant ~flags:Declareops.safe_flags id (ProjectionEntry entry,
+	let kn' = declare_constant id (ProjectionEntry entry,
 				       IsDefinition StructureComponent)
 	in
 	  assert(eq_constant kn kn')) kns; true,true
diff --git a/library/declare.mli b/library/declare.mli
index 41221d5c9..8dd24d278 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -54,11 +54,9 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 val declare_constant :
-  ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *)
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
-  ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *)
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
diff --git a/library/global.ml b/library/global.ml
index f4ee62b6e..c53611931 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,13 +77,14 @@ let globalize_with_summary fs f =
 
 let i2l = Label.of_id
 
-let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a)
-let push_named_def ~flags d = globalize (Safe_typing.push_named_def ~flags d)
+let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
+let push_named_def d = globalize (Safe_typing.push_named_def d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 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)
@@ -244,6 +245,14 @@ let is_template_polymorphic r =
   | IndRef ind -> Environ.template_polymorphic_ind ind env
   | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
 
+let is_type_in_type r =
+  let env = env() in
+  match r with
+  | VarRef id -> false
+  | ConstRef c -> Environ.type_in_type_constant c env
+  | IndRef ind -> Environ.type_in_type_ind ind env
+  | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env
+
 let current_dirpath () = 
   Safe_typing.current_dirpath (safe_env ())
 
diff --git a/library/global.mli b/library/global.mli
index 7c6cecb4e..247ca20b4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,11 +27,12 @@ val named_context : unit -> Context.Named.t
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
+val set_typing_flags : Declarations.typing_flags -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : flags:Declarations.typing_flags -> (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : flags:Declarations.typing_flags -> (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
+val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
 
 val add_constant :
   DirPath.t -> Id.t -> Safe_typing.global_declaration ->
@@ -116,6 +117,7 @@ val is_joined_environment : unit -> bool
 
 val is_polymorphic : Globnames.global_reference -> bool
 val is_template_polymorphic : Globnames.global_reference -> bool
+val is_type_in_type : Globnames.global_reference -> bool
 
 val type_of_global_in_context : Environ.env -> 
   Globnames.global_reference -> Constr.types Univ.in_universe_context
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index f69c4d821..c424fe122 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1432,7 +1432,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 8b3d3dc20..0cacb003d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -400,7 +400,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       Command.do_fixpoint ~flags:Declareops.safe_flags Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
 	   (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index a78eb1af7..99a165044 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -887,7 +887,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,pl,impls = Command.interp_mutual_inductive true indl []
+  let mie,pl,impls = Command.interp_mutual_inductive indl []
           false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1d7720454..403dcfd1a 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -592,9 +592,9 @@ let type_of_projection_knowing_arg env sigma p c ty =
 let control_only_guard env c =
   let check_fix_cofix e c = match kind_of_term c with
     | CoFix (_,(_,_,_) as cofix) ->
-      Inductive.check_cofix ~flags:Declareops.safe_flags e cofix
+      Inductive.check_cofix e cofix
     | Fix (_,(_,_,_) as fix) ->
-      Inductive.check_fix ~flags:Declareops.safe_flags e fix
+      Inductive.check_fix e fix
     | _ -> ()
   in
   let rec iter env c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 65f5b3fd0..b6a57785a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -72,17 +72,14 @@ open Inductiveops
 
 exception Found of int array
 
-(* spiwack: I chose [tflags] rather than [flags], like in the rest of
-   the code, for the argument name to avoid interference with the
-   argument for [inference_flags] also used in this module. *)
-let search_guard ~tflags loc env possible_indexes fixdefs =
+let search_guard loc env possible_indexes fixdefs =
   (* Standard situation with only one possibility for each fix. *)
   (* We treat it separately in order to get proper error msg. *)
   let is_singleton = function [_] -> true | _ -> false in
   if List.for_all is_singleton possible_indexes then
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
-    (try check_fix env ~flags:tflags fix
+    (try check_fix env fix
      with reraise ->
        let (e, info) = Errors.push reraise in
        let info = Loc.add_loc info loc in
@@ -101,7 +98,10 @@ let search_guard ~tflags loc env possible_indexes fixdefs =
                will be chosen). A more robust solution may be to raise an
                error when totality is assumed but the strutural argument is
                not specified. *)
-            try check_fix env ~flags:Declareops.safe_flags fix; raise (Found indexes)
+            try
+              let flags = { (typing_flags env) with Declarations.check_guarded = true } in
+              let env = Environ.set_typing_flags flags env in
+              check_fix env fix; raise (Found indexes)
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
@@ -617,13 +617,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	  let fixdecls = (names,ftys,fdefs) in
           let indexes =
             search_guard
-              ~tflags:Declareops.safe_flags
               loc env possible_indexes fixdecls
           in
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
 	  let cofix = (i,(names,ftys,fdefs)) in
-            (try check_cofix env ~flags:Declareops.safe_flags cofix
+            (try check_cofix env cofix
              with reraise ->
                let (e, info) = Errors.push reraise in
                let info = Loc.add_loc info loc in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 2c02b4a21..824bb11aa 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -22,7 +22,7 @@ open Misctypes
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
-val search_guard : tflags:Declarations.typing_flags ->
+val search_guard :
   Loc.t -> env -> int list list -> rec_declaration -> int array
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f03e6c6e9..52afa7f83 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -189,13 +189,13 @@ let rec execute env evdref cstr =
     | Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
-        check_fix env ~flags:Declareops.safe_flags fix;
+        check_fix env fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
-        check_cofix env ~flags:Declareops.safe_flags cofix;
+        check_cofix env cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9745a7925..ad67becd0 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -215,6 +215,12 @@ let print_polymorphism ref =
        else "not universe polymorphic") ]
   else []
 
+let print_type_in_type ref =
+  let unsafe = Global.is_type_in_type ref in
+  if unsafe then
+    [ pr_global ref ++ str " relies on an unsafe universe hierarchy"]
+  else []
+
 let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
     let eta = match recflag with
@@ -244,6 +250,7 @@ let print_name_infos ref =
     else
       [] in
   print_polymorphism ref @
+  print_type_in_type ref @
   print_primitive ref @
   type_info_for_implicit @
   print_renames_list (mt()) renames @
diff --git a/printing/printer.ml b/printing/printer.ml
index 509e982dc..8af2af98a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -775,7 +775,7 @@ module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let pr_assumptionset env s =
   if ContextObjectMap.is_empty s &&
-       engagement env = (PredicativeSet, StratifiedType) then
+       engagement env = PredicativeSet then
     str "Closed under the global context"
   else
     let safe_pr_constant env kn =
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6d84219d9..39f581082 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -79,7 +79,7 @@ let adjust_guardness_conditions const = function
                     List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
                 env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
-                search_guard ~tflags:Declareops.safe_flags Loc.ghost env
+                search_guard Loc.ghost env
                   possible_indexes fixdecls in
 		(mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index c05c5f6c2..fb32ecac3 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -293,7 +293,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
       in
-    if not (Declareops.constant_has_body cb) then
+    if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then
       let t = type_of_constant cb in
       let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
       ContextObjectMap.add (Axiom (Constant kn,l)) t accu
@@ -307,7 +307,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       accu
   | IndRef (m,_) | ConstructRef ((m,_),_) ->
       let mind = Global.lookup_mind m in
-      if mind.mind_checked_positive then
+      if mind.mind_typing_flags.check_guarded then
         accu
       else
         let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ff43cd495..5041d78a3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -145,9 +145,9 @@ let get_locality id = function
 | Local -> true
 | Global -> false
 
-let declare_global_definition ~flags ident ce local k pl imps =
+let declare_global_definition ident ce local k pl imps =
   let local = get_locality ident local in
-  let kn = declare_constant ~flags ident ~local (DefinitionEntry ce, IsDefinition k) in
+  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = Universes.register_universe_binders gr pl in
@@ -158,7 +158,7 @@ let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
-let declare_definition ~flags ident (local, p, k) ce pl imps hook =
+let declare_definition ident (local, p, k) ce pl imps hook =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
   let r = match local with
@@ -175,11 +175,11 @@ let declare_definition ~flags ident (local, p, k) ce pl imps hook =
     in
     gr
   | Discharge | Local | Global ->
-    declare_global_definition ~flags ident ce local k pl imps in
+    declare_global_definition ident ce local k pl imps in
   Lemmas.call_hook fix_exn hook local r
 
 let _ = Obligations.declare_definition_ref :=
-       (fun i k c imps hook -> declare_definition ~flags:Declareops.safe_flags i k c [] imps hook)
+       (fun i k c imps hook -> declare_definition i k c [] imps hook)
 
 let do_definition ident k pl bl red_option c ctypopt hook =
   let (ce, evd, pl', imps as def) =
@@ -203,7 +203,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ~flags:Declareops.safe_flags ident k ce pl' imps
+      ignore(declare_definition ident k ce pl' imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -549,7 +549,7 @@ let check_param = function
 | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
 | LocalRawAssum (nas, Generalized _, _) -> ()
 
-let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite =
+let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   let env0 = Global.env() in
@@ -631,7 +631,7 @@ let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite =
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
     mind_entry_universes = uctx;
-    mind_entry_check_positivity = chk; },
+  },
     pl, impls
 
 (* Very syntactical equality *)
@@ -716,19 +716,18 @@ type one_inductive_impls =
   Impargs.manual_explicitation list (* for inds *)*
   Impargs.manual_explicitation list list (* for constrs *)
 
-let do_mutual_inductive chk indl poly prv finite =
+let do_mutual_inductive indl poly prv finite =
   let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
-  let mie,pl,impls = interp_mutual_inductive chk indl ntns poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
   List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes;
-  (* If [chk] is [false] (i.e. positivity is assumed) declares itself
-     as unsafe. *)
-  if not chk then Feedback.feedback Feedback.AddedAxiom else ()
+  (* If positivity is assumed declares itself as unsafe. *)
+  if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
 (* 3c| Fixpoints and co-fixpoints *)
 
@@ -833,12 +832,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition ~flags f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref :=
-  (fun ?opaque k ctx f d t imps -> declare_fix ~flags:Declareops.safe_flags ?opaque k [] ctx f d t imps)
+  (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps)
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1139,7 +1138,7 @@ let interp_cofixpoint l ntns =
   check_recursive false  env evd fix;
   (fix,pl,Evd.evar_universe_context evd,info)
     
-let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1159,7 +1158,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let env = Global.env() in
-    let indexes = search_guard ~tflags:flags Loc.ghost env indexes fixdecls in
+    let indexes = search_guard Loc.ghost env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
@@ -1168,7 +1167,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
     let evd = Evd.restrict_universe_context evd vars in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix ~flags (local, poly, Fixpoint) pl ctx)
+    ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1176,7 +1175,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1202,7 +1201,7 @@ let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fix
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix ~flags (local, poly, CoFixpoint) pl ctx) 
+    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) 
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1269,11 +1268,9 @@ let do_program_recursive local p fixkind fixl ntns =
       in
       let indexes = 
         Pretyping.search_guard
-          ~tflags:Declareops.safe_flags
           Loc.ghost (Global.env ()) possible_indexes fixdecls in
       List.iteri (fun i _ ->
           Inductive.check_fix env
-                              ~flags:Declareops.safe_flags
                               ((indexes,i),fixdecls))
         fixl
   end in
@@ -1309,21 +1306,26 @@ let do_program_fixpoint local poly l =
 	errorlabstrm "do_program_fixpoint"
 	  (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_fixpoint ~flags local poly l =
+let check_safe () =
+  let open Declarations in
+  let flags = Environ.typing_flags (Global.env ()) in
+  flags.check_universes && flags.check_guarded
+
+let do_fixpoint local poly l =
   if Flags.is_program_mode () then do_program_fixpoint local poly l
   else
     let fixl, ntns = extract_fixpoint_components true l in
     let (_, _, _, info as fix) = interp_fixpoint fixl ntns in
     let possible_indexes =
       List.map compute_possible_guardness_evidences info in
-    declare_fixpoint ~flags local poly fix possible_indexes ntns;
-    if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else ()
+    declare_fixpoint local poly fix possible_indexes ntns;
+    if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
-let do_cofixpoint ~flags local poly l =
+let do_cofixpoint local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
     if Flags.is_program_mode () then
       do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
     else
       let cofix = interp_cofixpoint fixl ntns in
-      declare_cofixpoint ~flags local poly cofix ntns;
-      if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else ()
+      declare_cofixpoint local poly cofix ntns;
+      if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 2d27552a1..d35372429 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -36,7 +36,7 @@ val interp_definition :
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
       Universes.universe_binders * Impargs.manual_implicits
 
-val declare_definition : flags:Declarations.typing_flags -> Id.t -> definition_kind ->
+val declare_definition : Id.t -> definition_kind ->
   Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
@@ -91,7 +91,6 @@ type one_inductive_impls =
   Impargs.manual_implicits list (** for constrs *)
 
 val interp_mutual_inductive :
-  bool -> (* if [false], then positivity is assumed *)
   structured_inductive_expr -> decl_notation list -> polymorphic ->
     private_flag -> Decl_kinds.recursivity_kind ->
     mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
@@ -106,7 +105,6 @@ val declare_mutual_inductive_with_eliminations :
 (** Entry points for the vernacular commands Inductive and CoInductive *)
 
 val do_mutual_inductive :
-  bool -> (* if [false], then positivity is assumed *)
   (one_inductive_expr * decl_notation list) list -> polymorphic -> 
   private_flag -> Decl_kinds.recursivity_kind -> unit
 
@@ -150,13 +148,12 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  flags:Declarations.typing_flags ->
   locality -> polymorphic ->
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
-val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorphic -> 
+val declare_cofixpoint : locality -> polymorphic -> 
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
@@ -164,16 +161,16 @@ val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorp
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
-  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
+  (* When [false], assume guarded. *)
   locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
-  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
+  (* When [false], assume guarded. *)
   locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
 
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : flags:Declarations.typing_flags -> ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
   Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 46fb55b5f..e34f38eb3 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -115,10 +115,11 @@ let _ = at_exit print_memory_stat
 
 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 set_type_in_type () =
+  let typing_flags = Environ.typing_flags (Global.env ()) in
+  Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
 let engage () =
-  Global.set_engagement (!impredicative_set,!type_in_type)
+  Global.set_engagement !impredicative_set
 
 let set_batch_mode () = batch_mode := true
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 74361eb1c..fcb260f51 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -117,5 +117,4 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
     mind_entry_universes = univs;
-    mind_entry_check_positivity = mib.mind_checked_positive;
   }
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index a43758e3c..a48bbf89d 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -497,7 +497,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
 let declare_default_schemes kn =
   let mib = Global.lookup_mind kn in
   let n = Array.length mib.mind_packets in
-  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_checked_positive then
+  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded then
     declare_induction_schemes kn;
   if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
   if is_eq_flag() then try_declare_beq_scheme kn;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 3d15f2142..4d8d537f2 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -567,7 +567,7 @@ let declare_mutual_definition l =
 	    List.map3 compute_possible_guardness_evidences
               wfl fixdefs fixtypes in
 	  let indexes = 
-              Pretyping.search_guard ~tflags:Declareops.safe_flags
+              Pretyping.search_guard
               Loc.ghost (Global.env())
               possible_indexes fixdecls in
           Some indexes, 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 214d44d83..c9b46983e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -361,7 +361,7 @@ let structure_signature ctx =
 
 open Typeclasses
 
-let declare_structure chk finite poly ctx id idbuild paramimpls params arity template 
+let declare_structure finite poly ctx id idbuild paramimpls params arity template 
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
   let args = Context.Rel.to_extended_list nfields params in
@@ -387,7 +387,8 @@ let declare_structure chk finite poly ctx id idbuild paramimpls params arity tem
       mind_entry_polymorphic = poly;
       mind_entry_private = None;
       mind_entry_universes = ctx;
-      mind_entry_check_positivity = chk; } in
+    }
+  in
   let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
@@ -406,7 +407,7 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map get_name ctx)))
 
-let declare_class chk finite def poly ctx id idbuild paramimpls params arity 
+let declare_class finite def poly ctx id idbuild paramimpls params arity 
     template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -449,7 +450,7 @@ let declare_class chk finite def poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure chk BiFinite poly ctx (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -528,9 +529,8 @@ open Vernacexpr
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions 
-   or subinstances. When [chk] is false positivity is
-    assumed. *)
-let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
+   or subinstances. *)
+let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let cfs,priorities = List.split cfs in
   let coers,fs = List.split cfs in
@@ -551,14 +551,14 @@ let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
   let sign = structure_signature (fields@params) in
   let gr = match kind with
     | Class def ->
-	let gr = declare_class chk finite def poly ctx (loc,idstruc) idbuild
+	let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
 	  implpars params arity template implfs fields is_coe coers priorities sign in
 	gr
     | _ ->
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure chk finite poly ctx idstruc 
+	let ind = declare_structure finite poly ctx idstruc
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 525326237..b09425563 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -25,7 +25,6 @@ val declare_projections :
   (Name.t * bool) list * constant option list
 
 val declare_structure :
-  bool -> (** check positivity? *)
   Decl_kinds.recursivity_kind ->
   bool (** polymorphic?*) -> Univ.universe_context ->
   Id.t -> Id.t ->
@@ -39,7 +38,6 @@ val declare_structure :
   inductive
 
 val definition_structure :
-  bool -> (** check positivity? *)
   inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5131a4179..82fe9751e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -519,7 +519,7 @@ let vernac_assumption locality poly (local, kind) l nl =
   let status = do_assumptions kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_record chk k poly finite struc binders sort nameopt cfs =
+let vernac_record k poly finite struc binders sort nameopt cfs =
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
@@ -530,14 +530,13 @@ let vernac_record chk k poly finite struc binders sort nameopt cfs =
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure chk (k,poly,finite,struc,binders,cfs,const,sort))
+    ignore(Record.definition_structure (k,poly,finite,struc,binders,cfs,const,sort))
 
-(** When [chk] is false, positivity is assumed. When [poly] is true
-    the type is declared polymorphic. When [lo] is true, then the type
-    is declared private (as per the [Private] keyword). [finite]
+(** When [poly] is true the type is declared polymorphic. When [lo] is true,
+    then the type is declared private (as per the [Private] keyword). [finite]
     indicates whether the type is inductive, co-inductive or
     neither. *)
-let vernac_inductive chk poly lo finite indl =
+let vernac_inductive poly lo finite indl =
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
@@ -553,14 +552,14 @@ let vernac_inductive chk poly lo finite indl =
   | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
       Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
-      vernac_record chk (match b with Class true -> Class false | _ -> b)
+      vernac_record (match b with Class true -> Class false | _ -> b)
        poly finite id bl c oc fs
   | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
       let f =
 	let (coe, ((loc, id), ce)) = l in
 	let coe' = if coe then Some true else None in
   	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
-      in vernac_record chk (Class true) poly finite id bl c None [f]
+      in vernac_record (Class true) poly finite id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
       Errors.error "Definitional classes must have a single method"
   | [ ( id , bl , c , Class false, Constructors _), _ ] ->
@@ -574,19 +573,19 @@ let vernac_inductive chk poly lo finite indl =
       | _ -> Errors.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive chk indl poly lo finite
+    do_mutual_inductive indl poly lo finite
 
-let vernac_fixpoint ~flags locality poly local l =
+let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_fixpoint ~flags local poly l
+  do_fixpoint local poly l
 
-let vernac_cofixpoint ~flags locality poly local l =
+let vernac_cofixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_cofixpoint ~flags local poly l
+  do_cofixpoint local poly l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1731,8 +1730,6 @@ let vernac_load interp fname =
   try while true do interp (snd (parse_sentence input)) done
   with End_of_input -> ()
 
-let all_checks = Declareops.safe_flags
-
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
@@ -1769,9 +1766,9 @@ let interp ?proof ~loc locality poly c =
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
-  | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l
-  | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l
-  | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l
+  | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l
+  | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
+  | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe loc poly l