diff options
| author | Pierre-Marie Pédrot | 2015-10-06 17:51:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-06 17:51:57 +0200 |
| commit | c4db6fc1086d984fd983ff9a6797ad108d220b98 (patch) | |
| tree | cb57e5b678218e2baad13184544e645fd2e22cf5 /pretyping | |
| parent | 944c8de0bfe4048e0733a487e6388db4dfc9075a (diff) | |
| parent | 840155eafd9607c7656c80770de1e2819fe56a13 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping')
| -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 |