diff options
| author | Maxime Dénès | 2015-10-15 14:21:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-15 14:36:30 +0200 |
| commit | 44817bf722eacb0379bebc7e435bfafa503d574f (patch) | |
| tree | 210ffe37ee7e1d06f6a3b0b2a28b6bd192243c0d /pretyping/vnorm.ml | |
| parent | 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac (diff) | |
Fix #4346 2/2: VM casts were not inferring universe constraints.
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index f768e4feef..2c6ac7a292 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -312,3 +312,7 @@ and nf_cofix env cf = let cbv_vm env c t = let v = Vconv.val_of_constr env c in nf_val env v t + +let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = + Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb) + ~catch_incon:true ~pb env sigma t1 t2 |