From 28b5d3d14776fe5ce47b0da09edaf4c505872d1e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 6 Oct 2010 14:29:15 +0000 Subject: [PATCH] nAuto --> nnAuto --- matita/components/grafite_engine/grafiteEngine.ml | 4 ++-- matita/components/grafite_parser/grafiteParser.ml | 4 +--- 2 files changed, 3 insertions(+), 5 deletions(-) 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" -- 2.39.2