Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/native

Reviewed-by: ppedrot

2 files changed, 10 insertions, 12 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 30e1dc0611..3f68e3c78f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -318,13 +318,12 @@ and nf_atom_type env sigma atom =
   | Avar id ->
       mkVar id, Typeops.type_of_variable env id
   | Acase(ans,accu,p,bs) ->
-      let () = if Typeops.should_invert_case env ans.asw_ci then
-          (* TODO implement case inversion readback (properly reducing
-             it is a problem for the kernel) *)
-          CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.")
-      in
       let a,ta = nf_accu_type env sigma accu in
       let ((mind,_),u as ind),allargs = find_rectype_a env ta in
+      let iv = if Typeops.should_invert_case env ans.asw_ci then
+          CaseInvert {univs=u; args=allargs}
+        else NoInvert
+      in
       let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
       let nparams = mib.mind_nparams in
       let params,realargs = Array.chop nparams allargs in
@@ -344,7 +343,7 @@ and nf_atom_type env sigma atom =
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type p realargs a in
-      mkCase(ans.asw_ci, p, NoInvert, a, branchs), tcase
+      mkCase(ans.asw_ci, p, iv, a, branchs), tcase
   | Afix(tt,ft,rp,s) ->
       let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in
       let tt = Array.map fst tt and rt = Array.map snd tt in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b3f577b684..854a5ff63d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -263,12 +263,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
@@ -287,7 +286,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