@@ -392,7 +392,7 @@ simpleExpr syn =
392 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
392 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
393 <|> proofExpr syn
393 <|> proofExpr syn
394 <|> tacticsExpr syn
394 <|> tacticsExpr syn
395− <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)
395+ <|> try (do reserved "Type*"; return $ PUniverse AllTypes)
396 <|> do reserved "AnyType"; return $ PUniverse AllTypes
396 <|> do reserved "AnyType"; return $ PUniverse AllTypes
397 <|> PType <$> reservedFC "Type"
397 <|> PType <$> reservedFC "Type"
398 <|> do reserved "UniqueType"; return $ PUniverse UniqueType
398 <|> do reserved "UniqueType"; return $ PUniverse UniqueType
@@ -457,7 +457,7 @@ bracketed' open syn =
457 (ln, lnfc) <- name
457 (ln, lnfc) <- name
458 colonFC <- lcharFC ':'
458 colonFC <- lcharFC ':'
459 return (ln, lnfc, colonFC)
459 return (ln, lnfc, colonFC)
460− lty <- expr syn
460+ lty <- expr' syn
461 starsFC <- reservedOpFC "**"
461 starsFC <- reservedOpFC "**"
462 return (ln, lnfc, colonFC, lty, starsFC)
462 return (ln, lnfc, colonFC, lty, starsFC)
463 fc <- getFC
463 fc <- getFC