X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=74991bcb9cd957efe9b3da6c9bf23983d60000f8;hb=ef6a409b9cea2a3d0b0852ae3e69737566c91ba1;hp=7be30e407db19b1f918e46eb367080422e3114bd;hpb=52a0d6251f26055df769b179641fe077046e1f09;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 7be30e407..74991bcb9 100644
--- 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 ->
@@ -482,6 +484,7 @@ EXTEND
 ];
   auto_fixed_param: [
    [ IDENT "paramodulation"
+   | IDENT "demod"
    | IDENT "fast_paramod"
    | IDENT "paramod"
    | IDENT "slir"