X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Ftranscript%2Fv8Lexer.mll;h=5a90aabf75b91769e47c214b7864679f958b8028;hb=b3fe1b05014341773ab30cf14fdffa8a7e2f298c;hp=0fea9c9eba0eb47b4caa9eb61f0b63ef2088d524;hpb=ad17757edcc6cf75be576268fab8cf52751d679a;p=helm.git

diff --git a/components/binaries/transcript/v8Lexer.mll b/components/binaries/transcript/v8Lexer.mll
index 0fea9c9eb..5a90aabf7 100644
--- a/components/binaries/transcript/v8Lexer.mll
+++ b/components/binaries/transcript/v8Lexer.mll
@@ -13,7 +13,7 @@ let RAWID = QT [^ '"']* QT
 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      }
@@ -26,19 +26,19 @@ rule token = parse
    | "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      }
@@ -49,7 +49,7 @@ rule token = parse
    | "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   }