New experimental commit: metavariables representation is changed again,

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualLexer.mll

diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
index 3e256b2cf7aab75b055b2c0f012589b8d6ae91e9..31878bfe6e83d68405f1759597f7d5ac5840d4d4 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
+++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
@@ -71,12 +71,17 @@ rule token =
   | indtyuri    { INDTYURI (indtyuri_of_uri ("cic:" ^ L.lexeme lexbuf)) }
   | indconuri   { INDCONURI (indconuri_of_uri("cic:" ^ L.lexeme lexbuf)) }
   | num         { NUM (int_of_string (L.lexeme lexbuf)) }
-  | '?' num     { META (int_of_string (L.lexeme lexbuf)) }
+  | '?' num     { let lexeme = L.lexeme lexbuf in
+                   META
+                    (int_of_string
+                     (String.sub lexeme 1 (String.length lexeme - 1))) }
   | ":>"        { CAST }
   | ":="        { LETIN }
   | '?'         { IMPLICIT }
   | '('         { LPAREN }
   | ')'         { RPAREN }
+  | '['         { LBRACKET }
+  | ']'         { RBRACKET }
   | '{'         { LCURLY }
   | '}'         { RCURLY }
   | ';'         { SEMICOLON }
@@ -85,5 +90,6 @@ rule token =
   | ':'         { COLON }
   | '.'         { DOT }
   | "->"        { ARROW }
+  | "_"         { NONE }
   | eof         { EOF }
 {}