Define *file() syntax for tactic constructors.

[goals.git] / src / lexer.mll

diff --git a/src/lexer.mll b/src/lexer.mll
index d0f4a1d..a9b11d1 100644 (file)
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -52,6 +52,9 @@ rule read =
     | "{"     { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }
     | "let"   { LET }
+    | "*" id  { let id = Lexing.lexeme lexbuf in
+                let len = String.length id in
+                TACTIC (String.sub id 1 (len-1)) }
     | id      { ID (Lexing.lexeme lexbuf) }
     | _       { raise (SyntaxError ("unexpected character: " ^
                                     Lexing.lexeme lexbuf)) }