diff options
| author | Pierre-Marie Pédrot | 2020-04-30 14:10:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-30 14:10:16 +0200 |
| commit | d436c45a19de2f91aad94f492b547225f8c5b305 (patch) | |
| tree | b666e829b6545ba38170dcf79276714dd89cbe32 /kernel/environ.ml | |
| parent | 010ef152611977770fa137ed5980205d412febe5 (diff) | |
| parent | 7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 (diff) | |
Merge PR #12107: Remove mod_constraints field of module body
Reviewed-by: ppedrot
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 cf01711fe7..d6d52dbc2b 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 } |