bugfix

diff --git a/TypeChecker.hs b/TypeChecker.hs
index a6d36946b750ca730611b4c1a142d626b8189381..d5d180eabbbbaa6a2945f2b49dbb5a216bfd7e7a 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -169,8 +169,8 @@ check a t = case (a,t) of
       local (addSubs iis) $ localM (addTele tele) $ do\r
         checkSystemWith ts $ \alpha talpha ->\r
           local (faceEnv alpha) $ do\r
-            rhoAlpha <- asks env\r
-            check (Ter t rhoAlpha) talpha\r
+            -- NB: the type doesn't depend on is\r
+            check (Ter t rho) talpha\r
         rho' <- asks env\r
         checkCompSystem (evalSystem rho' ts)\r
   (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do\r