diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:21:45 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:36:30 +0200 |
| commit | 44817bf722eacb0379bebc7e435bfafa503d574f (patch) | |
| tree | 210ffe37ee7e1d06f6a3b0b2a28b6bd192243c0d /pretyping/pretyping.ml | |
| parent | 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac (diff) | |
Fix #4346 2/2: VM casts were not inferring universe constraints.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e1e8982e1..f6c186728 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -929,14 +929,11 @@ 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 if not (occur_existential cty || occur_existential tval) then - begin - 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 + let (evd,b) = Vnorm.vm_infer_conv env !evdref cty tval in + if b then (evdref := evd; cj) + else + error_actual_type_loc loc env !evdref cj tval (ConversionFailed (env,cty,tval)) - end else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> |