From 5b17a67ffd16485adf2e66a6241b72e91ed15621 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 26 Sep 2005 15:14:59 +0000 Subject: [PATCH] new signature of auto_tac, with a new optional argument "full", to invoke the new paramodulation --- helm/matita/matitaEngine.ml | 8 ++++---- helm/matita/matitaGui.ml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index b06504052..4e48df807 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -65,8 +65,8 @@ let tactic_of_ast ast = | GrafiteAst.Absurd (_, term) -> Tactics.absurd term | GrafiteAst.Apply (_, term) -> Tactics.apply term | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width,paramodulation) -> - AutoTactic.auto_tac ?depth ?width ?paramodulation + | GrafiteAst.Auto (_,depth,width,paramodulation,full) -> + AutoTactic.auto_tac ?depth ?width ?paramodulation ?full ~dbd:(MatitaDb.instance ()) () | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what @@ -227,8 +227,8 @@ let disambiguate_tactic status tactic = let cic = disambiguate_term status_ref term in GrafiteAst.Apply (loc, cic) | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc - | GrafiteAst.Auto (loc,depth,width,paramodulation) -> - GrafiteAst.Auto (loc,depth,width,paramodulation) + | GrafiteAst.Auto (loc,depth,width,paramodulation,full) -> + GrafiteAst.Auto (loc,depth,width,paramodulation,full) | GrafiteAst.Change (loc, pattern, with_what) -> let with_what = disambiguate_lazy_term status_ref with_what in let pattern = disambiguate_pattern status_ref pattern in diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 5d223208f..8351426f8 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -549,7 +549,7 @@ class gui () = (tac_w_term (A.Transitivity (loc, hole))); connect_button tbar#assumptionButton (tac (A.Assumption loc)); connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole))); - connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); + connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None))); MatitaGtkMisc.toggle_widget_visibility ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) ~check:main#tacticsBarMenuItem; -- 2.39.2