Add typechecking for glueElem

diff --git a/TypeChecker.hs b/TypeChecker.hs
index ad26bc388ace1851a1b3f061ae42b775b78032f4..9f89bb5a8bf00721389e68c515ae27539b4d5628 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -205,10 +205,10 @@ check a t = case (a,t) of
     check VU a\r
     rho <- asks env\r
     checkGlue (eval rho a) ts\r
-  -- (VGlue va ts,GlueElem u us) -> do\r
-  --   check va u\r
-  --   vu <- evalTyping u\r
-  --   checkGlueElem vu ts us\r
+  (VGlue va ts,GlueElem u us) -> do\r
+    check va u\r
+    vu <- evalTyping u\r
+    checkGlueElem vu ts us\r
   _ -> do\r
     v <- infer t\r
     unlessM (v === a) $\r