- Procedural: we specify more unifiers for apply to help higher-order unification

[helm.git] / helm / software / components / binaries / transcript / grafiteLexer.mll

diff --git a/helm/software/components/binaries/transcript/grafiteLexer.mll b/helm/software/components/binaries/transcript/grafiteLexer.mll
index bfa818e301bfa429a5275562663f8b723d9070a3..ac3055bc53707bf7cc952f145f1b060895535313 100644 (file)
--- a/helm/software/components/binaries/transcript/grafiteLexer.mll
+++ b/helm/software/components/binaries/transcript/grafiteLexer.mll
@@ -62,12 +62,14 @@ rule token = parse
    | "default"         { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
    | "include"         { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
    | "inline"          { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
+   | "pump"            { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
    | "qed"             { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
    | "elim"            { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
    | "apply"           { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
    | "intros"          { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
    | "assume"          { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
    | "the"             { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
+   | "rewrite"         { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
    | IDENT             { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s   }
    | "." SPC           { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s   }
    | "."               { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s   }