META parsing was completely broken. Fixed.

[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 107ff356ff9ed02be71bf55db8e17b9ae2702f1d..8c1a5b4aed55f0067a0a337d89690a17f08a2404 100644 (file)
--- 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")
@@ -71,7 +71,10 @@ 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 }