menu fised

[helm.git] / components / content_pres / cicNotationParser.ml

diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml
index 088d1b69d690562e4ce74281f3109cccdee259d0..461e2fc9f755e9b0f868188ac4b535accd4b996d 100644 (file)
--- a/components/content_pres/cicNotationParser.ml
+++ b/components/content_pres/cicNotationParser.ml
@@ -224,7 +224,7 @@ let level_of precedence associativity =
   in
   string_of_int precedence ^ assoc_string
 
-type rule_id = Token.t Gramext.g_symbol list
+type rule_id = Grammar.token Gramext.g_symbol list
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23
@@ -452,12 +452,17 @@ 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, []
+    [ id = IDENT -> Ast.Pattern (id, None, [])
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
-        id, None, vars
+       Ast.Pattern (id, None, vars)
+    | id = IDENT; vars = LIST1 possibly_typed_name ->
+       Ast.Pattern (id, None, vars)
+    | SYMBOL "_" -> Ast.Wildcard
     ]
   ];
   binder: [