allow overshadowing of names

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 31235687fc49f991af9117ff382ec97beb2c5937..979fbbc12c9fb3a6edd97f94ac98b2f28002d92d 100644 (file)
--- 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\r
 checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do\r
   ns' <- asks names\r
-  mapM_ checkFresh js\r
+  -- mapM_ checkFresh js\r
   let us   = mkVars ns' tele nu\r
       vus  = map snd us\r
       js'  = map Atom js\r
@@ -339,7 +339,7 @@ checkFresh i = do
 checkPath :: Val -> Ter -> Typing (Val,Val)\r
 checkPath v (Path i a) = do\r
   rho <- asks env\r
-  checkFresh i\r
+  -- checkFresh i\r
   local (addSub (i,Atom i)) $ check (v @@ i) a\r
   return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a)\r
 checkPath v t = do\r