X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2FcicNotationParser.ml;h=d110bda9a65d10b6cabfc0074a798e5bd7040786;hb=6ff514ec3bdc39bd0afbdfb210290a670a20a60d;hp=088d1b69d690562e4ce74281f3109cccdee259d0;hpb=f084490a318c45b1a4090a85119f54c463aec063;p=helm.git

diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml
index 088d1b69d..d110bda9a 100644
--- a/components/content_pres/cicNotationParser.ml
+++ b/components/content_pres/cicNotationParser.ml
@@ -452,12 +452,15 @@ EXTEND
         id, Some typ
     | arg = single_arg -> arg, None
     | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
+        Ast.Ident ("_", None), Some typ
     ]
   ];
   match_pattern: [
     [ id = IDENT -> id, None, []
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
         id, None, vars
+    | id = IDENT; vars = LIST1 possibly_typed_name -> id, None, vars
     ]
   ];
   binder: [