diff options
| author | Matthieu Sozeau | 2015-10-06 09:58:20 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-06 10:01:19 +0200 |
| commit | df9caebb04fb681ec66b79c41ae01918cd2336de (patch) | |
| tree | f1712aa32ab470692d35a440c7d2a45cfcc37ec2 | |
| parent | 07f4e6b07775052cc1c5dc34cdfa7ad4eacfa94f (diff) | |
Univs (pretyping): call vm_compute/native_compute with the current
universe graph
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f18657da82..2efd8fe413 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -903,7 +903,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in if not (occur_existential cty || occur_existential tval) then begin - try + try + let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj with Reduction.NotConvertible -> error_actual_type_loc loc env !evdref cj tval @@ -915,6 +916,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in let evars = Nativenorm.evars_of_evar_map !evdref in + let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in begin try ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj |