diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 9678d25..b86caae 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1007,7 +1007,7 @@ directive fname indents e <- extension atEnd indents pure (Extension e) - <|> do exactIdent "default" + <|> do keyword "default" tot <- totalityOpt atEnd indents pure (DefaultTotality tot)