From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 6 Oct 2010 14:29:15 +0000 (+0000)
Subject: nAuto --> nnAuto
X-Git-Tag: make_still_working~2800
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=28b5d3d14776fe5ce47b0da09edaf4c505872d1e;p=helm.git

nAuto --> nnAuto
---

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index ee030a215..ad90b2b2e 100644
--- 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 3a0edb7ac..89a09fc50 100644
--- 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"