@@ -390,7 +390,7 @@ pSyntaxRule syn
390390 when (length ns /= length (nub ns))
391391 $ fail "Repeated variable in syntax rule"
392392 lchar '='
393− tm <- pExpr (impOK syn)
393+ tm <- pTExpr (impOK syn)
394394 pTerminator
395395 return (Rule (mkSimple syms) tm sty)
396396 where
@@ -908,10 +908,11 @@ mkType (NS n s) = NS (mkType n) s
908908noImp syn = syn { implicitAllowed = False }
909909impOK syn = syn { implicitAllowed = True }
910910
911−pTSig syn = do lchar ':'
912− cs <- if implicitAllowed syn then pConstList syn else return []
913− sc <- pExpr syn
914− return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
911+pTSig syn = do lchar ':'; pTExpr syn
912+
913+pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []
914+ sc <- pExpr syn
915+ return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
915916
916917pLambda syn = do lchar '\\'
917918 try (do xt <- tyOptDeclList syn