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

diff --git a/proofs/logic.ml b/proofs/logic.ml
index f159395177..cb67d42bdc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -265,15 +265,12 @@ let collect_meta_variables c =
   let rec collrec deep acc c = match kind c with
     | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
     | Cast(c,_,_) -> collrec deep acc c
-    | Case(ci,p,iv,c,br) ->
-      (* Hack assuming only two situations: the legacy one that branches,
-         if with Metas, are Meta, and the new one with eta-let-expanded
-         branches *)
-      let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in
-      let acc = Constr.fold (collrec deep) acc p in
+    | Case(ci,u,pms,p,iv,c,br) ->
+      let acc = Array.fold_left (collrec deep) acc pms in
+      let acc = Constr.fold (collrec deep) acc (snd p) in
       let acc = Constr.fold_invert (collrec deep) acc iv in
       let acc = Constr.fold (collrec deep) acc c in
-      Array.fold_left (collrec deep) acc br
+      Array.fold_left (fun accu (_, br) -> collrec deep accu br) acc br
     | App _ -> Constr.fold (collrec deep) acc c
     | Proj (_, c) -> collrec deep acc c
     | _ -> Constr.fold (collrec true) acc c
@@ -369,15 +366,16 @@ let rec mk_refgoals ~check env sigma goalacc conclty trm =
         let ty = EConstr.Unsafe.to_constr ty in
           (acc',ty,sigma,c)
 
-      | Case (ci,p,iv,c,lf) ->
+      | Case (ci, u, pms, p, iv, c, lf) ->
         (* XXX Is ignoring iv OK? *)
+        let (ci, p, iv, c, lf) = Inductive.expand_case env (ci, u, pms, p, iv, c, lf) in
         let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in
         let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in
         let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else mkCase (ci,p',iv,c',lf')
+          else mkCase (Inductive.contract_case env (ci,p',iv,c',lf'))
         in
         (acc'',conclty',sigma, ans)
 
@@ -418,14 +416,15 @@ and mk_hdgoals ~check env sigma goalacc trm =
         let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
         (acc'',conclty',sigma, ans)
 
-    | Case (ci,p,iv,c,lf) ->
+    | Case (ci, u, pms, p, iv, c, lf) ->
         (* XXX is ignoring iv OK? *)
+        let (ci, p, iv, c, lf) = Inductive.expand_case env (ci, u, pms, p, iv, c, lf) in
         let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in
         let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
-          else mkCase (ci,p',iv,c',lf')
+          else mkCase (Inductive.contract_case env (ci,p',iv,c',lf'))
         in
         (acc'',conclty',sigma, ans)