Back-porting from new matita:

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index d7aae9ee8c1bc9021686b619ae096943a3d4c4a0..941bb221871192ae6ecaf32f7d9dcc75fd54dbb9 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -155,6 +155,7 @@ EXTEND
     | 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 ]
   ];
@@ -289,7 +290,10 @@ EXTEND
     | 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 ->