X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=d110bda9a65d10b6cabfc0074a798e5bd7040786;hb=380284d5b85bd218f812bc0f9725061912c291f6;hp=088d1b69d690562e4ce74281f3109cccdee259d0;hpb=14724f9aab44f1b150a5509743a43cb6693d493e;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 088d1b69d..d110bda9a 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/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: [