nAuto --> nnAuto

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index ee030a215e0a3b26af3be5c06cee0bc5c3d7a03f..ad90b2b2e1db3c66c735fc0c7fbb93d8094d9485 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -778,9 +778,9 @@ let eval_ng_tac tac =
           (text,prefix_len,concl))
        ) seqs)
   | GrafiteAst.NAuto (_loc, (None,a)) -> 
-      NAuto.auto_tac ~params:(None,a) ?trace_ref:None
+      NnAuto.auto_tac ~params:(None,a) ?trace_ref:None
   | GrafiteAst.NAuto (_loc, (Some l,a)) ->
-      NAuto.auto_tac
+      NnAuto.auto_tac
        ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
   | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
   | GrafiteAst.NCases (_loc, what, where) ->

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 3a0edb7ac59ee3071166848080dfbc002be163db..89a09fc50cda8fe22f7379fb5c5cef08d0ae975a 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -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"