diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 03c9cb4be6..e497b7904a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -467,14 +467,22 @@ let same_flags { [@warning "+9"] let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b) +let set_type_in_type b = map_universes (UGraph.set_type_in_type b) let set_typing_flags c env = if same_flags env.env_typing_flags c then env - else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c } + else + let env = { env with env_typing_flags = c } in + let env = set_cumulative_sprop c.cumulative_sprop env in + let env = set_type_in_type (not c.check_universes) env in + env let set_cumulative_sprop b env = set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env +let set_type_in_type b env = + set_typing_flags {env.env_typing_flags with check_universes=not b} env + let set_allow_sprop b env = { env with env_stratification = { env.env_stratification with env_sprop_allowed = b } } |