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, 4 insertions, 7 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 802a32b0e7..83e41a63ec 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -548,7 +548,9 @@ let rec execute env cstr =
     | Construct c ->
       cstr, type_of_constructor env c
 
-    | Case (ci,p,iv,c,lf) ->
+    | Case (ci, u, pms, p, iv, c, lf) ->
+        (** FIXME: change type_of_case to handle the compact form *)
+        let (ci, p, iv, c, lf) = expand_case env (ci, u, pms, p, iv, c, lf) in
         let c', ct = execute env c in
         let iv' = match iv with
           | NoInvert -> NoInvert
@@ -563,7 +565,7 @@ let rec execute env cstr =
         let lf', lft = execute_array env lf in
         let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in
         let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr
-          else mkCase(ci',p',iv',c',lf')
+          else mkCase (Inductive.contract_case env (ci',p',iv',c',lf'))
         in
         cstr, t
 
@@ -720,11 +722,6 @@ let judge_of_inductive env indu =
 let judge_of_constructor env cu =
   make_judge (mkConstructU cu) (type_of_constructor env cu)
 
-let judge_of_case env ci pj iv cj lfj =
-  let lf, lft = dest_judgev lfj in
-  let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in
-  make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t
-
 (* Building type of primitive operators and type *)
 
 let type_of_prim_const env _u c =