X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualLexer.mll;h=5ab17fa80ce5e5879bf4a33320b3acc5b36802cc;hb=0de1b960f42ac368414b7405a79e7933445ee8af;hp=01ddd0cf302acdede1f9b14f086864077677ce10;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index 01ddd0cf3..5ab17fa80 100644
--- 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 }