[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
reduction_kind: [
- [ IDENT "reduce" -> `Reduce
+ [ IDENT "normalize" -> `Normalize
+ | IDENT "reduce" -> `Reduce
| IDENT "simplify" -> `Simpl
- | IDENT "whd" -> `Whd
- | IDENT "normalize" -> `Normalize ]
+ | IDENT "unfold"; t = OPT term -> `Unfold t
+ | IDENT "whd" -> `Whd ]
];
sequent_pattern_spec: [
[ hyp_paths =
[ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
];
notation: [
- [ s = QSTRING;
+ [ dir = OPT direction; s = QSTRING;
assoc = OPT associativity; prec = OPT precedence;
IDENT "for";
p2 =
| None -> default_precedence
| Some prec -> prec
in
- (add_raw_attribute ~text:s
- (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
- assoc, prec, p2)
+ let p1 =
+ add_raw_attribute ~text:s
+ (CicNotationParser.parse_level1_pattern (Stream.of_string s))
+ in
+ (dir, p1, assoc, prec, p2)
]
];
level3_term: [
]
];
interpretation: [
- [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+ [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
(s, args, t)
]
];
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
let uris = List.map UriManager.uri_of_string uris in
GrafiteAst.Default (loc,what,uris)
- | IDENT "notation"; (l1, assoc, prec, l2) = notation ->
- GrafiteAst.Notation (loc, l1, assoc, prec, l2)
+ | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
+ GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2)
| IDENT "interpretation"; id = QSTRING;
(symbol, args, l3) = interpretation ->
GrafiteAst.Interpretation (loc, id, (symbol, args), l3)