GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
- ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
+ new_name: [
+ [ id = IDENT -> Some id
+ | SYMBOL "_" -> None ]
+ ];
+ ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
tactic_term_list1: [
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
| IDENT "auto"; params = auto_params ->
GrafiteAst.Auto (loc,params)
| IDENT "cases"; what = tactic_term;
- (num, idents) = intros_spec ->
- GrafiteAst.Cases (loc, what, idents)
+ specs = intros_spec ->
+ GrafiteAst.Cases (loc, what, specs)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+ | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
| None -> None, [], Some Ast.UserInput
| Some pattern -> pattern
in
- GrafiteAst.Elim (loc, what, using, pattern, num, idents)
+ GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
- GrafiteAst.ElimType (loc, what, using, num, idents)
+ GrafiteAst.ElimType (loc, what, using, (num, idents))
| IDENT "exact"; t = tactic_term ->
GrafiteAst.Exact (loc, t)
| IDENT "exists" ->
GrafiteAst.Fold (loc, kind, t, p)
| IDENT "fourier" ->
GrafiteAst.Fourier loc
- | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+ | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.FwdSimpl (loc, hyp, idents)
| IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
GrafiteAst.Generalize (loc,p,id)
| IDENT "id" -> GrafiteAst.IdTac loc
| IDENT "intro"; ident = OPT IDENT ->
- let idents = match ident with None -> [] | Some id -> [id] in
- GrafiteAst.Intros (loc, Some 1, idents)
- | IDENT "intros"; (num, idents) = intros_spec ->
- GrafiteAst.Intros (loc, num, idents)
+ let idents = match ident with None -> [] | Some id -> [Some id] in
+ GrafiteAst.Intros (loc, (Some 1, idents))
+ | IDENT "intros"; specs = intros_spec ->
+ GrafiteAst.Intros (loc, specs)
| IDENT "inversion"; t = tactic_term ->
GrafiteAst.Inversion (loc, t)
| IDENT "lapply";