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, 17 insertions, 3 deletions

diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 335c2e5e68..e2721b4822 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -68,6 +68,15 @@ let subst_univs_fn_constr f c =
       let u' = fi u in
         if u' == u then t
         else (changed := true; mkConstructU (c, u'))
+    | Case (ci, u, pms, p, NoInvert, c, br) ->
+      let u' = fi u in
+      if u' == u then map aux t
+      else (changed := true; map aux (mkCase (ci, u', pms, p, NoInvert, c, br)))
+    | Case (ci, u, pms, p, CaseInvert{univs;args}, c, br) ->
+      let u' = fi u in
+      let univs' = fi univs in
+      if u' == u && univs' == univs then map aux t
+      else (changed := true; map aux (mkCase (ci, u', pms, p, CaseInvert {univs = univs'; args}, c, br)))
     | _ -> map aux t
   in
   let c' = aux c in
@@ -147,10 +156,15 @@ let nf_evars_and_universes_opt_subst f subst =
     | Sort (Type u) ->
       let u' = Univ.subst_univs_universe subst u in
       if u' == u then c else mkSort (sort_of_univ u')
-    | Case (ci,p,CaseInvert {univs;args},t,br) ->
+    | Case (ci, u, pms, p, NoInvert, t, br) ->
+      let u' = Instance.subst_fn lsubst u in
+      if u' == u then map aux c
+      else Constr.map aux (mkCase (ci, u', pms, p, NoInvert, t, br))
+    | Case (ci,u,pms,p,CaseInvert {univs;args},t,br) ->
+      let u' = Instance.subst_fn lsubst u in
       let univs' = Instance.subst_fn lsubst univs in
-      if univs' == univs then Constr.map aux c
-      else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br))
+      if u' == u && univs' == univs then Constr.map aux c
+      else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},t,br))
     | Array (u,elems,def,ty) ->
       let u' = Univ.Instance.subst_fn lsubst u in
       let elems' = CArray.Smart.map aux elems in