constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90" -> t ] ];
new_name: [
- [ id = IDENT -> Some id
- | SYMBOL "_" -> None ]
+ [ SYMBOL "_" -> None
+ | id = IDENT -> Some id ]
];
ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
tactic_term_list1: [
];
level3_term: [
[ u = URI -> N.UriPattern (UriManager.uri_of_string u)
+ | IMPLICIT -> N.ImplicitPattern
| id = IDENT -> N.VarPattern id
- | SYMBOL "_" -> N.ImplicitPattern
| LPAREN; terms = LIST1 SELF; RPAREN ->
(match terms with
| [] -> assert false