New option "demod" for auto.

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index ef354789a25dab4d0304990ebfd6a23b257c4575..74991bcb9cd957efe9b3da6c9bf23983d60000f8 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -484,6 +484,7 @@ EXTEND
 ];
   auto_fixed_param: [
    [ IDENT "paramodulation"
+   | IDENT "demod"
    | IDENT "fast_paramod"
    | IDENT "paramod"
    | IDENT "slir"