From: Anders Mörtberg <mortberg@chalmers.se>
Date: Thu, 19 Mar 2015 07:58:26 +0000 (+0100)
Subject: Use checkPath when checking IdP
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9281901b42d4fb56786d44091a70c6744c49ab9c;p=cubicaltt.git

Use checkPath when checking IdP
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 1a33798..473657d 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -154,13 +154,10 @@ check a t = case (a,t) of
     local (addDecls d) $ check a e
   (_,Undef _) -> return ()
   (VU,IdP a e0 e1) -> case a of
-    Path i b -> do
-      rho <- asks env
-      when (i `elem` support rho)
-        (throwError (show i ++ " is already declared"))
-      local (addSub (i,Atom i)) $ check VU b
-      check (eval (Sub rho (i,Dir 0)) b) e0
-      check (eval (Sub rho (i,Dir 1)) b) e1
+    Path{} -> do
+      (b0,b1) <- checkPath a
+      check b0 e0
+      check b1 e1
     _ -> do
       b <- infer a
       case b of