New tactics ncut and nlapply.

[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 6b80c32cf0c411ef948933e9bf7778fc7aada208..c9ece6dba31b1aa1b2260aae49d7f6aa8f67869f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -256,10 +256,12 @@ EXTEND
     | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term -> 
         G.NConstructor (loc,
            (match num with None -> None | Some x -> Some (int_of_string x)),l)
+    | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         G.NElim (loc, what, where)
     | IDENT "ngeneralize"; p=pattern_spec ->
         G.NGeneralize (loc, p)
+    | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
         where = pattern_spec ->
         G.NLetIn (loc,where,t,name)