X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.ml;h=21031d002fc10fba43eb915623f054d45743ecd0;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=1dab53582f590d6addf47af680be5cfe25580799;hpb=d34061fd1c820139fad38c39dee6377e5057bf26;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index 1dab53582..21031d002 100644
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -69,7 +69,6 @@ let regexp delim_end = "\\]"
 let regexp qkeyword = "'" ( ident | pident ) "'"
 
 let regexp implicit = '?'
-let regexp implicit_vector = "..."
 let regexp placeholder = '%'
 let regexp meta = implicit number
 
@@ -317,7 +316,6 @@ and level2_ast_token =
      let s = Ulexing.utf8_lexeme lexbuf in
       return lexbuf ("META", String.sub s 1 (String.length s - 1))
   | implicit -> return lexbuf ("IMPLICIT", "")
-  | implicit_vector -> return lexbuf ("IMPLICITVECTOR", "")
   | placeholder -> return lexbuf ("PLACEHOLDER", "")
   | ident -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "IDENT"
   | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)