@@ -390,7 +390,7 @@ pSyntaxRule syn
390 when (length ns /= length (nub ns))
390 when (length ns /= length (nub ns))
391 $ fail "Repeated variable in syntax rule"
391 $ fail "Repeated variable in syntax rule"
392 lchar '='
392 lchar '='
393− tm <- pExpr (impOK syn)
393+ tm <- pTExpr (impOK syn)
394 pTerminator
394 pTerminator
395 return (Rule (mkSimple syms) tm sty)
395 return (Rule (mkSimple syms) tm sty)
@@ -908,10 +908,11 @@ mkType (NS n s) = NS (mkType n) s
908noImp syn = syn { implicitAllowed = False }
908noImp syn = syn { implicitAllowed = False }
909impOK syn = syn { implicitAllowed = True }
909impOK syn = syn { implicitAllowed = True }
911−pTSig syn = do lchar ':'
911+pTSig syn = do lchar ':'; pTExpr syn
912− cs <- if implicitAllowed syn then pConstList syn else return []
913+pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
913− sc <- pExpr syn
914+ sc <- pExpr syn
914− return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
915+ return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
916pLambda syn = do lchar '\\'
917pLambda syn = do lchar '\\'
917 try (do xt <- tyOptDeclList syn
918 try (do xt <- tyOptDeclList syn