parameter sintax added to axiom statement

[helm.git] / helm / software / components / content_pres / cicNotationLexer.ml

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index 1dab53582f590d6addf47af680be5cfe25580799..21031d002fc10fba43eb915623f054d45743ecd0 100644 (file)
--- 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)