Moving the typing_flags to the environment.

14 files changed, 102 insertions, 102 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 639cd061b..ef4d398c1 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) } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 032e71359..65aaa3f7b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -45,16 +45,14 @@ 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 universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
@@ -211,6 +209,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
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7ce1cea27..0edcb34de 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,6 +50,7 @@ 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
 
@@ -214,6 +215,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/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 a7c6ef057..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,8 +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 flags = { flags with check_universes = flags.check_universes && not (type_in_type env) } in
+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
@@ -354,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
@@ -369,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 =
@@ -410,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 ->
@@ -451,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
@@ -466,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 *)