diff options
Diffstat (limited to 'pretyping/typing.ml')
-rw-r--r-- | pretyping/typing.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 6bd75c93d..68f9610d1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -215,10 +215,7 @@ let judge_of_cast env sigma cj k tj = uj_type = expected_type } let enrich_env env sigma = - let penv = Environ.pre_env env in - let penv' = Pre_env.({ penv with env_stratification = - { penv.env_stratification with env_universes = Evd.universes sigma } }) in - Environ.env_of_pre_env penv' + set_universes env @@ Evd.universes sigma let check_fix env sigma pfix = let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in |