From: Simon Huber <hubsim@gmail.com>
Date: Thu, 30 Apr 2015 13:32:12 +0000 (+0200)
Subject: allow overshadowing of names
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d01c143873b1476ec244a9e8279ef631636f35a0;p=cubicaltt.git

allow overshadowing of names
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 3123568..979fbbc 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -307,7 +307,7 @@ checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do
   local (addBranch (zip ns us) nu) $ check (app f (VCon c us)) e
 checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do
   ns' <- asks names
-  mapM_ checkFresh js
+  -- mapM_ checkFresh js
   let us   = mkVars ns' tele nu
       vus  = map snd us
       js'  = map Atom js
@@ -339,7 +339,7 @@ checkFresh i = do
 checkPath :: Val -> Ter -> Typing (Val,Val)
 checkPath v (Path i a) = do
   rho <- asks env
-  checkFresh i
+  -- checkFresh i
   local (addSub (i,Atom i)) $ check (v @@ i) a
   return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a)
 checkPath v t = do