Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)

Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle

1 files changed, 10 insertions, 17 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3707a75157..f82b754c59 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -75,30 +75,23 @@ let share_univs cache r u l =
   let (u', args) = share cache r l in
     mkApp (instantiate_my_gr r (Instance.append u' u), args)
 
-let update_case cache ci iv modlist =
-  match share cache (IndRef ci.ci_ind) modlist with
-  | exception Not_found -> ci, iv
-  | u, l ->
-    let iv = match iv with
-      | NoInvert -> NoInvert
-      | CaseInvert {univs; args;} ->
-        let univs = Instance.append u univs in
-        let args = Array.append l args in
-        CaseInvert {univs; args;}
-    in
-    { ci with ci_npar = ci.ci_npar + Array.length l }, iv
-
 let is_empty_modlist (cm, mm) =
   Cmap.is_empty cm && Mindmap.is_empty mm
 
 let expmod_constr cache modlist c =
   let share_univs = share_univs cache in
-  let update_case = update_case cache in
   let rec substrec c =
     match kind c with
-      | Case (ci,p,iv,t,br) ->
-        let ci,iv = update_case ci iv modlist in
-        Constr.map substrec (mkCase (ci,p,iv,t,br))
+      | Case (ci, u, pms, p, iv, t, br) ->
+        begin match share cache (IndRef ci.ci_ind) modlist with
+        | (u', prefix) ->
+          let u = Instance.append u' u in
+          let pms = Array.append prefix pms in
+          let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in
+          Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br))
+        | exception Not_found ->
+          Constr.map substrec c
+        end
 
       | Ind (ind,u) ->
           (try