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

diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index c62bc73e41..e208ba9a5c 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -67,10 +67,13 @@ let unif env evd t1 t2=
           | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
           | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
               Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
-          | Case (_,pa,_,ca,va),Case (_,pb,_,cb,vb)->
-            Queue.add (pa,pb) bige;
-            Queue.add (ca,cb) bige;
-            let l=Array.length va in
+          | Case (cia,ua,pmsa,pa,iva,ca,va),Case (cib,ub,pmsb,pb,ivb,cb,vb)->
+            let env = Global.env () in
+            let (cia,pa,iva,ca,va) = EConstr.expand_case env evd (cia,ua,pmsa,pa,iva,ca,va) in
+            let (cib,pb,iva,cb,vb) = EConstr.expand_case env evd (cib,ub,pmsb,pb,ivb,cb,vb) in
+              Queue.add (pa,pb) bige;
+              Queue.add (ca,cb) bige;
+              let l=Array.length va in
                 if not (Int.equal l (Array.length vb)) then
                   raise (UFAIL (nt1,nt2))
                 else