rebuilt against ocaml 3.08.3

[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualLexer.mll

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index 01ddd0cf302acdede1f9b14f086864077677ce10..5ab17fa80ce5e5879bf4a33320b3acc5b36802cc 100644 (file)
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -81,6 +81,7 @@ rule token =
   | "\\Set"     { SET }
   | "\\Prop"    { PROP }
   | "\\Type"    { TYPE }
+  | "\\CProp"   { CPROP }
   | ident       { ID (unquote (L.lexeme lexbuf)) }
   | conuri      { CONURI
                    (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) }
@@ -90,6 +91,11 @@ rule token =
                    (indtyuri_of_uri ("cic:" ^ (unquote (L.lexeme lexbuf)))) }
   | indconuri   { INDCONURI
                    (indconuri_of_uri("cic:" ^ (unquote (L.lexeme lexbuf)))) }
+  | num '.'     {
+                  let lexeme = L.lexeme lexbuf in
+                  RNUM (int_of_string
+                    (String.sub lexeme 0 (String.length lexeme - 1)))
+                }
   | num         { NUM (int_of_string (L.lexeme lexbuf)) }
   | '?' num     { let lexeme = L.lexeme lexbuf in
                    META
@@ -108,6 +114,8 @@ rule token =
   | "\\lambda"  { LAMBDA }
   | "\\pi"      { PROD }
   | "\\forall"  { PROD }
+  | "\\eqt"     { EQT }
+  | "\\neqt"    { NEQT }
   | ':'         { COLON }
   | '.'         { DOT }
   | "\\to"      { ARROW }
@@ -115,6 +123,10 @@ rule token =
   | dollar      { DOLLAR }
   | eof         { EOF }
   (* Arithmetical operators *)
+  | "+."        { RPLUS }
+  | "-."        { RMINUS }
+  | "*."        { RTIMES }
+  | "/."        { RDIV }
   | '+'         { PLUS }
   | '-'         { MINUS }
   | '*'         { TIMES }