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, 11 insertions, 6 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 4778bf1121..c5ac57a2cd 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -355,21 +355,26 @@ let rec map_kn f f' c =
       | Construct (((kn,i),j),u) ->
           let kn' = f kn in
           if kn'==kn then c else mkConstructU (((kn',i),j),u)
-      | Case (ci,p,iv,ct,l) ->
+      | Case (ci,u,pms,p,iv,ct,l) ->
           let ci_ind =
             let (kn,i) = ci.ci_ind in
             let kn' = f kn in
             if kn'==kn then ci.ci_ind else kn',i
           in
-          let p' = func p in
+          let f_ctx (nas, c as d) =
+            let c' = func c in
+            if c' == c then d else (nas, c')
+          in
+          let pms' = Array.Smart.map func pms in
+          let p' = f_ctx p in
           let iv' = map_invert func iv in
           let ct' = func ct in
-          let l' = Array.Smart.map func l in
-            if (ci.ci_ind==ci_ind && p'==p && iv'==iv
+          let l' = Array.Smart.map f_ctx l in
+            if (ci.ci_ind==ci_ind && pms'==pms && p'==p && iv'==iv
                 && l'==l && ct'==ct)then c
             else
-              mkCase ({ci with ci_ind = ci_ind},
-                      p',iv',ct', l')
+              mkCase ({ci with ci_ind = ci_ind}, u,
+                      pms',p',iv',ct', l')
       | Cast (ct,k,t) ->
           let ct' = func ct in
           let t'= func t in