X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2FgrafiteLexer.mll;h=ac3055bc53707bf7cc952f145f1b060895535313;hb=cfb41205e930ede65c1d19ec7ec6f252e0803d55;hp=bfa818e301bfa429a5275562663f8b723d9070a3;hpb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;p=helm.git

diff --git a/helm/software/components/binaries/transcript/grafiteLexer.mll b/helm/software/components/binaries/transcript/grafiteLexer.mll
index bfa818e30..ac3055bc5 100644
--- 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   }