X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Flexer.mll;h=273b09dbf5f959021e21848e3cfd66e50b4743ea;hb=214f84c3b07227767fef90934895a167b15113a1;hp=a9b11d1047eaeb12ef82758f801cbff517efef2a;hpb=7f776dee39a35732964a30091e55aa795169bca5;p=goals.git

diff --git a/src/lexer.mll b/src/lexer.mll
index a9b11d1..273b09d 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -51,10 +51,10 @@ rule read =
     | '"'     { read_string (Ast.Substs.create ()) lexbuf }
     | "{"     { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }
+    | "tactic" { TACTIC_KEYWORD }
     | "let"   { LET }
-    | "*" id  { let id = Lexing.lexeme lexbuf in
-                let len = String.length id in
-                TACTIC (String.sub id 1 (len-1)) }
+    | "*" id  { (* NB: The initial '*' is part of the name. *)
+                TACTIC (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }
     | _       { raise (SyntaxError ("unexpected character: " ^
                                     Lexing.lexeme lexbuf)) }