nAuto --> nnAuto

[helm.git] / matita / components / grafite_parser / grafiteParser.ml

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 941bb221871192ae6ecaf32f7d9dcc75fd54dbb9..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"
@@ -730,16 +728,6 @@ EXTEND
            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
       | IDENT "auto"; params = auto_params ->
           G.AutoInteractive (loc,params)
-      | [ IDENT "whelp"; "match" ] ; t = term -> 
-          G.WMatch (loc,t)
-      | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
-          G.WInstance (loc,t)
-      | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> 
-          G.WLocate (loc,id)
-      | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
-          G.WElim (loc, t)
-      | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
-          G.WHint (loc,t)
       ]
     ];
     alias_spec: [