...

[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 faa17124edd09053a0634267af03ae4fdb3acb35..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 ]
   ];
@@ -276,6 +277,7 @@ EXTEND
        | 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))
@@ -288,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 ->
@@ -315,7 +320,7 @@ EXTEND
             (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)])