--- /dev/null
+{
+ module P = V8Parser
+
+ let out t s = () (* prerr_endline (t ^ " " ^ s) *)
+}
+
+let QT = '"'
+let SPC = [' ' '\t' '\n' '\r']+
+let ALPHA = ['A'-'Z' 'a'-'z' '_']
+let FIG = ['0'-'9']
+let ID = ALPHA (ALPHA | FIG | "\'")*
+let RAWID = QT [^ '"']* QT
+let NUM = "-"? FIG+
+
+rule token = parse
+ | "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 }
+ | "Definition" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
+ | "Fixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s }
+ | "Qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
+ | "Defined" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
+ | "Proof" { let s = Lexing.lexeme lexbuf in out "PRF" s; P.PROOF s }
+ | "Variable" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR 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 "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 "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 }
+ | "Load" { let s = Lexing.lexeme lexbuf in out "LOAD" s; P.LOAD s }
+ | "Set" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
+ | "Implicit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s }
+ | "Notation" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT 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 "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 }
+ | "(*" { let s = Lexing.lexeme lexbuf in out "OQ" s; P.OQ s }
+ | "*)" { let s = Lexing.lexeme lexbuf in out "CQ" s; P.CQ s }
+ | "(" { let s = Lexing.lexeme lexbuf in out "OP" s; P.OP s }
+ | ")" { let s = Lexing.lexeme lexbuf in out "CP" s; P.CP s }
+ | "{" { let s = Lexing.lexeme lexbuf in out "OC" s; P.OC s }
+ | "}" { let s = Lexing.lexeme lexbuf in out "CC" s; P.CC s }
+ | ";" { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s }
+ | ":" { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s }
+ | _ { let s = Lexing.lexeme lexbuf in out "SPEC" s; P.EXTRA s }
+ | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF }