}
let QT = '"'
-let SPC = [' ' '\t' '\n']+
+let SPC = [' ' '\t' '\n' '\r']+
let ALPHA = ['A'-'Z' 'a'-'z' '_']
let FIG = ['0'-'9']
let ID = ALPHA (ALPHA | FIG | "\'")*
let NUM = "-"? FIG+
rule token = parse
- | "Let" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
+ | "Let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s }
| "Remark" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
| "Lemma" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
| "Theorem" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
| "Variables" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s }
| "Hypothesis" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s }
| "Hypotheses" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s }
- | "Axiom" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s }
+ | "Axiom" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s }
| "Inductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s }
| "Record" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s }
| "Section" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "End" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "Hint" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "Unset" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "Print" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "Opaque" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "Transparent" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "Ltac" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "Tactic" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
- | "Declare" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s }
+ | "End" { let s = Lexing.lexeme lexbuf in out "END" s; P.END s }
+ | "Hint" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
+ | "Unset" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
+ | "Print" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
+ | "Opaque" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
+ | "Transparent" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
+ | "Ltac" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
+ | "Tactic" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
+ | "Declare" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
| "Require" { let s = Lexing.lexeme lexbuf in out "REQ" s; P.REQ s }
| "Export" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s }
| "Import" { let s = Lexing.lexeme lexbuf in out "IP" s; P.IP s }
| "Infix" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s }
| "Identity" { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s }
| "Coercion" { let s = Lexing.lexeme lexbuf in out "CO" s; P.COERC s }
- | "let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s }
+ | "let" { let s = Lexing.lexeme lexbuf in out "ABBR" s; P.ABBR s }
| "in" { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN s }
| SPC { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s }
| ID { let s = Lexing.lexeme lexbuf in out "ID" s; P.IDENT s }
| RAWID { let s = Lexing.lexeme lexbuf in out "STR" s; P.STR s }
| NUM { let s = Lexing.lexeme lexbuf in out "INT" s; P.INT s }
| ":=" { let s = Lexing.lexeme lexbuf in out "DEF" s; P.DEF s }
+ | ":>" { let s = Lexing.lexeme lexbuf in out "COE" s; P.COE s }
| "." ID { let s = Lexing.lexeme lexbuf in out "AC" s; P.AC s }
| "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s }
| "." eof { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s }