Added syntax for ninversion tactic (still experimental).

[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 7be30e407db19b1f918e46eb367080422e3114bd..ef354789a25dab4d0304990ebfd6a23b257c4575 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -268,6 +268,8 @@ EXTEND
         G.NElim (loc, what, where)
     | IDENT "ngeneralize"; p=pattern_spec ->
         G.NGeneralize (loc, p)
+    | IDENT "ninversion"; what = tactic_term ; where = pattern_spec ->
+        G.NInversion (loc, what, where)
     | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
         where = pattern_spec ->