X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Flexer.mll;h=9ea2f741f191a83066ffa1313ccd61df6d9e2114;hb=98b795ddf06271fa8018edcd0bd15960871828fd;hp=6afa40c051c89e225e3fd193d32b6fd212d0512d;hpb=deb7edaccefe379139818e8b241844b9a0571651;p=goals.git

diff --git a/src/lexer.mll b/src/lexer.mll
index 6afa40c..9ea2f74 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -53,10 +53,11 @@ rule read =
     | "{"     { read_code false (Ast.Substs.create ()) (ref 1) lexbuf }
     | "@{"    { read_code true  (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }
-    | "tactic"
-              { TACTIC_KEYWORD }
+    | "predicate"
+              { PREDICATE }
     | "function"
               { FUNCTION }
+    | "pure"  { PURE }
     | "let"   { LET }
     | "include"
               { INCLUDE }
@@ -70,8 +71,9 @@ rule read =
               { STRING_KEYWORD }
     | "strings"
               { STRINGS }
-    | "*" id  { (* NB: The initial '*' is part of the name. *)
-                TACTIC (Lexing.lexeme lexbuf) }
+    | "is-" id
+              { (* NB: The initial 'is-' is part of the name. *)
+                PRED (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }
     | _       { raise (SyntaxError ("unexpected character: " ^
                                     Lexing.lexeme lexbuf)) }