| id = IDENT -> Some id ]
];
ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
+ ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
tactic_term_list1: [
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
| Some `Trace ->
G.NMacro(loc,
G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
+ | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
| IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
| IDENT "screenshot"; fname = QSTRING ->
G.NMacro(loc,G.Screenshot (loc, fname))
| IDENT "ncut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
(* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
| IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
- | IDENT "ndestruct" -> G.NTactic(loc,[G.NDestruct loc])
+ | IDENT "ndestruct"; just = OPT [ dom = ident_list1 -> dom ];
+ exclude = OPT [ IDENT "skip"; skip = ident_list1 -> skip ]
+ -> let exclude' = match exclude with None -> [] | Some l -> l in
+ G.NTactic(loc,[G.NDestruct (loc,just,exclude')])
| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
G.NTactic(loc,[G.NElim (loc, what, where)])
| IDENT "ngeneralize"; p=pattern_spec ->
(List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
G.NTactic(loc,[G.NBlock (loc,l)])
| IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc])
- | SYMBOL "#"; n=IDENT -> G.NTactic(loc,[ G.NIntro (loc,n)])
+ | SYMBOL "#"; ns=LIST0 IDENT -> G.NTactic(loc,[ G.NIntros (loc,ns)])
| SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
| SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
| SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])