X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=components%2Fcontent_pres%2FcicNotationParser.ml;h=461e2fc9f755e9b0f868188ac4b535accd4b996d;hb=refs%2Ftags%2F0.4.95;hp=d110bda9a65d10b6cabfc0074a798e5bd7040786;hpb=8f5b25b6091f1e240f37de5355e7a99b756e98e8;p=helm.git diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml index d110bda9a..461e2fc9f 100644 --- 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 @@ -457,10 +457,12 @@ EXTEND ] ]; match_pattern: [ - [ id = IDENT -> id, None, [] + [ id = IDENT -> Ast.Pattern (id, None, []) | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN -> - id, None, vars - | id = IDENT; vars = LIST1 possibly_typed_name -> id, None, vars + Ast.Pattern (id, None, vars) + | id = IDENT; vars = LIST1 possibly_typed_name -> + Ast.Pattern (id, None, vars) + | SYMBOL "_" -> Ast.Wildcard ] ]; binder: [