]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
ported debian stuff to ocaml 3.08
[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualLexer.mll
index 06bbab076ec8c3b501d30dfa3e49d196a29b6c82..5ab17fa80ce5e5879bf4a33320b3acc5b36802cc 100644 (file)
@@ -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)))) }
@@ -114,6 +115,7 @@ rule token =
   | "\\pi"      { PROD }
   | "\\forall"  { PROD }
   | "\\eqt"     { EQT }
+  | "\\neqt"    { NEQT }
   | ':'         { COLON }
   | '.'         { DOT }
   | "\\to"      { ARROW }