From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 plugins/firstorder/unify.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 9c3debe48f..c62bc73e41 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -67,10 +67,10 @@ 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 (_,pa,_,ca,va),Case (_,pb,_,cb,vb)->
+            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
-- 
cgit v1.2.3