X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=695db149e3f0c2bc722629d589b8bfc39f61adb9;hb=6daa2cc113783aaba53d82c47fe7107988d76e11;hp=14032d4512994e54c2c72fd404848a1ebee7e72b;hpb=df753672ee6c511b6ce721c2124e3294d0a28dbd;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 14032d451..695db149e 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -608,18 +608,21 @@ EXTEND
     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
         id, Some typ
     | arg = single_arg -> arg, None
+    | id = PIDENT -> Ast.Ident (id, None), None
     | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
+        Ast.Ident (id, None), Some typ
     | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
         Ast.Ident ("_", None), Some typ
     ]
   ];
   match_pattern: [
-    [ id = IDENT -> Ast.Pattern (id, None, [])
+    [ SYMBOL "_" -> Ast.Wildcard
+    | id = IDENT -> Ast.Pattern (id, None, [])
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
        Ast.Pattern (id, None, vars)
     | id = IDENT; vars = LIST1 possibly_typed_name ->
        Ast.Pattern (id, None, vars)
-    | SYMBOL "_" -> Ast.Wildcard
     ]
   ];
   binder: [
@@ -690,9 +693,11 @@ EXTEND
     ]
   ];
   binder_vars: [
-    [ vars = [
-          l = LIST1 single_arg SEP SYMBOL "," -> l
-        | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
+    [ vars = [ l =
+        [ l = LIST1 single_arg SEP SYMBOL "," -> l
+        | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> 
+            List.map (fun x -> Ast.Ident(x,None)) l
+      ] -> l ];
       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
     ]
   ];