| 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 ]
];
| 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 ->
try
f ()
with
- | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
- | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ | Ploc.Exc (_, End_of_file) -> raise End_of_file
+ | Ploc.Exc (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
- | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
+ | Ploc.Exc (floc, HExtlib.Localized(_,exn)) ->
raise
(HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
- | Stdpp.Exc_located (floc, exn) ->
+ | Ploc.Exc (floc, exn) ->
raise
(HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))