From 716da638633f01d6a5b52c05e0bd6adc86385b60 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 May 2005 13:47:30 +0000 Subject: [PATCH] attached auto --- helm/matita/matita.glade | 8 ++++---- helm/matita/matitaEngine.ml | 5 +++-- helm/matita/matitaGui.ml | 2 +- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 47c9d9e9e..2704d164d 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1044,7 +1044,7 @@ Copyright (C) 2005, - 102 + 109 True True 0 @@ -1213,7 +1213,7 @@ Copyright (C) 2005, - 50 + 55 True ElimType True @@ -1736,8 +1736,8 @@ Copyright (C) 2005, 0 - False - False + True + True diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index f3ac49e16..59d1c7b79 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -43,7 +43,8 @@ let tactic_of_ast = function Tactics.elim_intros_simpl term | TacticAst.ElimType (_, term) -> Tactics.elim_type term | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what -(* | TacticAst.Auto _ -> Tactics.auto_new ~dbd *) + | TacticAst.Auto (_,num) -> + AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ()) | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what (* (* TODO Zack a lot more of tactics to be implemented here ... *) @@ -286,7 +287,7 @@ let disambiguate_tactic status = function *) | TacticAst.Intros (loc, num, names) -> status, TacticAst.Intros (loc, num, names) - | TacticAst.Auto loc -> status, TacticAst.Auto loc + | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num) | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc | TacticAst.Assumption loc -> status, TacticAst.Assumption loc | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 5a6377b3b..ec4d042ff 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -144,7 +144,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, hole))); - connect_button tbar#autoButton (tac (A.Auto loc)); + connect_button tbar#autoButton (tac (A.Auto (loc,None))); (* quit *) self#setQuitCallback (fun () -> exit 0); (* log *) -- 2.39.2