Implement -include (optional include) command.

[goals.git] / src / lexer.mll

diff --git a/src/lexer.mll b/src/lexer.mll
index 617c10f..84f2af2 100644 (file)
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -54,6 +54,7 @@ rule read =
     | "tactic" { TACTIC_KEYWORD }
     | "let"   { LET }
     | "include" { INCLUDE }
+    | "-include" { OPTINCLUDE }
     | "*" id  { (* NB: The initial '*' is part of the name. *)
                 TACTIC (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }