From: Claudio Sacerdoti Coen Date: Mon, 29 Apr 2002 10:06:06 +0000 (+0000) Subject: META parsing was completely broken. Fixed. X-Git-Tag: V_0_3_0_debian_8~121 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d89ef07d5045594c88e3f217a7df1a9ac8f9284;p=helm.git META parsing was completely broken. Fixed. --- diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll index 3e256b2cf..8c1a5b4ae 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll +++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll @@ -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 }