diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index de8692ff21..93f1b051ab 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -279,6 +279,9 @@ let indices_matter env = env.env_typing_flags.indices_matter let universes env = env.env_stratification.env_universes let universes_lbound env = env.env_stratification.env_universes_lbound +let set_universes g env = + {env with env_stratification = {env.env_stratification with env_universes=g}} + let set_universes_lbound env lbound = let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in { env with env_stratification } |