From d01c143873b1476ec244a9e8279ef631636f35a0 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 30 Apr 2015 15:32:12 +0200 Subject: [PATCH] allow overshadowing of names --- TypeChecker.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.34.1