X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualLexer.mll;h=06bbab076ec8c3b501d30dfa3e49d196a29b6c82;hb=71284ef6c56c909e7205543f3fe8b916517f79b0;hp=01ddd0cf302acdede1f9b14f086864077677ce10;hpb=f80986dd44466287251d58367b021870de22ba7b;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..06bbab076 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -90,6 +90,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 +113,7 @@ rule token =
   | "\\lambda"  { LAMBDA }
   | "\\pi"      { PROD }
   | "\\forall"  { PROD }
+  | "\\eqt"     { EQT }
   | ':'         { COLON }
   | '.'         { DOT }
   | "\\to"      { ARROW }
@@ -115,6 +121,10 @@ rule token =
   | dollar      { DOLLAR }
   | eof         { EOF }
   (* Arithmetical operators *)
+  | "+."        { RPLUS }
+  | "-."        { RMINUS }
+  | "*."        { RTIMES }
+  | "/."        { RDIV }
   | '+'         { PLUS }
   | '-'         { MINUS }
   | '*'         { TIMES }