X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualLexer.mll;h=1be084795a11505eb80764da93da88e1ad79d5b6;hb=f41a5585a648d57e4d8a24d664b0a5ce5d591148;hp=8c1a5b4aed55f0067a0a337d89690a17f08a2404;hpb=1d89ef07d5045594c88e3f217a7df1a9ac8f9284;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
index 8c1a5b4ae..1be084795 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
+++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
@@ -49,7 +49,7 @@
  ;;
 }
 let num = ['1'-'9']['0'-'9']* | '0'
-let alfa = ['A'-'Z' 'a'-'z' '_']
+let alfa = ['A'-'Z' 'a'-'z' '_' ''' '-']
 let ident = alfa (alfa | num)*
 let baseuri = '/'(ident '/')* ident '.'
 let conuri = baseuri ("con" | "var")
@@ -80,6 +80,8 @@ rule token =
   | '?'         { IMPLICIT }
   | '('         { LPAREN }
   | ')'         { RPAREN }
+  | '['         { LBRACKET }
+  | ']'         { RBRACKET }
   | '{'         { LCURLY }
   | '}'         { RCURLY }
   | ';'         { SEMICOLON }
@@ -88,5 +90,6 @@ rule token =
   | ':'         { COLON }
   | '.'         { DOT }
   | "->"        { ARROW }
+  | "_"         { NONE }
   | eof         { EOF }
 {}