Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.

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