Downgrading level of infix notations involving \sup.

[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..74991bcb9cd957efe9b3da6c9bf23983d60000f8 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 ->
@@ -482,6 +484,7 @@ EXTEND
 ];
   auto_fixed_param: [
    [ IDENT "paramodulation"
+   | IDENT "demod"
    | IDENT "fast_paramod"
    | IDENT "paramod"
    | IDENT "slir"