@@ -392,7 +392,7 @@ simpleExpr syn =
392392 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
393393 <|> proofExpr syn
394394 <|> tacticsExpr syn
395− <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)
395+ <|> try (do reserved "Type*"; return $ PUniverse AllTypes)
396396 <|> do reserved "AnyType"; return $ PUniverse AllTypes
397397 <|> PType <$> reservedFC "Type"
398398 <|> do reserved "UniqueType"; return $ PUniverse UniqueType
@@ -457,7 +457,7 @@ bracketed' open syn =
457457 (ln, lnfc) <- name
458458 colonFC <- lcharFC ':'
459459 return (ln, lnfc, colonFC)
460− lty <- expr syn
460+ lty <- expr' syn
461461 starsFC <- reservedOpFC "**"
462462 return (ln, lnfc, colonFC, lty, starsFC)
463463 fc <- getFC