Moving the typing_flags to the environment.

1 files changed, 21 insertions, 22 deletions

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