diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index efe1efd74e..bad718860a 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -262,12 +262,11 @@ and nf_stk ?from:(from=0) env sigma c t stk = | Zswitch sw :: stk -> assert (from = 0) ; let ci = sw.sw_annot.Vmvalues.ci in - let () = if Typeops.should_invert_case env ci then - (* TODO implement case inversion readback (properly reducing - it is a problem for the kernel) *) - CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.") - in let ((mind,_ as ind), u), allargs = find_rectype_a env t in + let iv = if Typeops.should_invert_case env ci then + CaseInvert {univs=u; args=allargs} + else NoInvert + in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in @@ -286,7 +285,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs c in - nf_stk env sigma (mkCase(ci, p, NoInvert, c, branchs)) tcase stk + nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; let p' = Projection.make p true in |