LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
string_of_int v | v = IDENT -> v ] -> i,v ] ->
GrafiteAst.Auto (loc,params)
LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
string_of_int v | v = IDENT -> v ] -> i,v ] ->
GrafiteAst.Auto (loc,params)
- | IDENT "clear"; id = IDENT ->
- GrafiteAst.Clear (loc,id)
+ | IDENT "clear"; ids = LIST1 IDENT ->
+ GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
- (num, idents) = intros_spec ->
+ | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
+ idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
let to_spec id = GrafiteAst.Ident id in
GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
| IDENT "discriminate"; t = tactic_term ->
let to_spec id = GrafiteAst.Ident id in
GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
| IDENT "discriminate"; t = tactic_term ->