diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 16 |
1 files changed, 1 insertions, 15 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 38bb56b92b..501ac99ff3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -275,7 +275,6 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let indices_matter env = env.env_typing_flags.indices_matter -let check_template env = env.env_typing_flags.check_template let universes env = env.env_stratification.env_universes let universes_lbound env = env.env_stratification.env_universes_lbound @@ -446,7 +445,6 @@ let same_flags { share_reduction; enable_VM; enable_native_compiler; - check_template; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -455,8 +453,7 @@ let same_flags { indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && - enable_native_compiler == alt.enable_native_compiler && - check_template == alt.check_template + enable_native_compiler == alt.enable_native_compiler [@warning "+9"] let set_typing_flags c env = (* Unsafe *) @@ -588,9 +585,6 @@ let polymorphic_pind (ind,u) env = let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes -let template_checked_ind (mind,_i) env = - (lookup_mind mind env).mind_typing_flags.check_template - let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true @@ -799,14 +793,6 @@ let get_template_polymorphic_variables env r = | IndRef ind -> template_polymorphic_variables ind env | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env -let is_template_checked env r = - let open Names.GlobRef in - match r with - | VarRef _id -> false - | ConstRef _c -> false - | IndRef ind -> template_checked_ind ind env - | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env - let is_type_in_type env r = let open Names.GlobRef in match r with |