X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Flexer.mll;h=66c6b9feef221ef2b0d22b58c5a52123222ed972;hb=976bb1b35d77f3058df3c25c1e2a4767147d606b;hp=f2d083063258da907818ec93939309a44712a302;hpb=84972c63d0dbc5a0da05ae08a5b99a9ad81baadc;p=goals.git

diff --git a/src/lexer.mll b/src/lexer.mll
index f2d0830..66c6b9f 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -52,10 +52,15 @@ rule read =
     | '"'     { read_string (Ast.Substs.create ()) lexbuf }
     | "{"     { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }
-    | "tactic" { TACTIC_KEYWORD }
+    | "tactic"
+              { TACTIC_KEYWORD }
+    | "function"
+              { FUNCTION }
     | "let"   { LET }
-    | "include" { INCLUDE }
-    | "-include" { OPTINCLUDE }
+    | "include"
+              { INCLUDE }
+    | "-include"
+              { OPTINCLUDE }
     | "*" id  { (* NB: The initial '*' is part of the name. *)
                 TACTIC (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }