diff options
| author | Pierre-Marie Pédrot | 2018-05-28 20:11:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-28 20:11:06 +0200 |
| commit | a205bb9f2a93396aad154ec50f6f122cbd46811c (patch) | |
| tree | cd1ad9834fa9e6391193b377cc4533f9eba702c5 /pretyping/typing.ml | |
| parent | 81535edc4b21015bd63d23e57ca9d707b4b71f6b (diff) | |
| parent | 131ac2af3778a741f5f33e212ef4a57f7a91d20a (diff) | |
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
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 6bd75c93d5..68f9610d18 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 |