| "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 }