]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/grafite_parser/grafiteParser.ml
nAuto --> nnAuto
[helm.git] / matita / components / grafite_parser / grafiteParser.ml
index 3a0edb7ac59ee3071166848080dfbc002be163db..89a09fc50cda8fe22f7379fb5c5cef08d0ae975a 100644 (file)
@@ -520,11 +520,9 @@ EXTEND
   ]
 ];
   auto_fixed_param: [
-   [ IDENT "paramodulation"
-   | IDENT "demod"
+   [ IDENT "demod"
    | IDENT "fast_paramod"
    | IDENT "paramod"
-   | IDENT "slir"
    | IDENT "depth"
    | IDENT "width"
    | IDENT "size"