From: Simon Huber <hubsim@gmail.com>
Date: Thu, 23 Apr 2015 12:57:28 +0000 (+0200)
Subject: bugix: take the border of the system where is=js
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=97c1fb49dd36e19e795e4faf9d05c13d1f7b282e;p=cubicaltt.git

bugix: take the border of the system where is=js
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 08e75b0..93557f4 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -304,11 +304,11 @@ checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do
       vus  = map snd us
       js'  = map Atom js
       vts  = evalSystem (subs (upds nu us) (zip is js')) ts
-      vfts = intersectionWith app (border g ts) vts
+      vfts = intersectionWith app (border g vts) vts
   local (addSubs (zip js js') . addBranch (zip ns vus) nu) $ do
     check (app f (VPCon c va vus js')) e
     ve  <- evalTyping e -- TODO: combine with next line?
-    unlessM (border ve ts === vfts) $
+    unlessM (border ve vts === vfts) $
       throwError $ "Faces of branch don't match"
 
 checkFormula :: Formula -> Typing ()