From 2e872b47e36edfa97137e6e7bc4bdcab3d1612a0 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Sat, 18 Apr 2015 05:26:04 +0200 Subject: [PATCH] bugfix --- TypeChecker.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TypeChecker.hs b/TypeChecker.hs index a6d3694..d5d180e 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -169,8 +169,8 @@ check a t = case (a,t) of local (addSubs iis) $ localM (addTele tele) $ do checkSystemWith ts $ \alpha talpha -> local (faceEnv alpha) $ do - rhoAlpha <- asks env - check (Ter t rhoAlpha) talpha + -- NB: the type doesn't depend on is + check (Ter t rho) talpha rho' <- asks env checkCompSystem (evalSystem rho' ts) (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do -- 2.34.1