diff options
| -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 |