From 6b7f04b45232e6c690cacf5815c85c39de1f52b3 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 5 Nov 2004 11:06:46 +0000 Subject: [PATCH] filled toolbar and implemented buttons behaviours --- helm/matita/matita.glade | 637 +++++++++++++++++++++++++++-- helm/matita/matita.ml | 39 +- helm/matita/matitaGeneratedGui.ml | 158 ++++++- helm/matita/matitaGeneratedGui.mli | 90 +++- helm/matita/matitaGui.ml | 20 + helm/matita/matitaGui.mli | 1 + helm/matita/matitaInterpreter.ml | 38 +- 7 files changed, 891 insertions(+), 92 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 7c272a828..4ecd6d46a 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -449,10 +449,10 @@ - 130 + 150 450 True - ToolBar + Tactics GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE False @@ -471,86 +471,524 @@ False - + True False 0 - + True - GTK_BUTTONBOX_DEFAULT_STYLE - 0 + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - - 120 + True - True - True - button1 - True - GTK_RELIEF_NORMAL - True + True + True + False + + + + True + Intros + True + intros + True + GTK_RELIEF_NORMAL + True + + + + False + False + - + True - True - True - button2 - True - GTK_RELIEF_NORMAL - True + True + True + False + + + + True + Apply + True + apply + True + GTK_RELIEF_NORMAL + True + + + + False + False + - + True - True - True - button3 - True - GTK_RELIEF_NORMAL - True + True + True + False + + + + True + Exact + True + exact + True + GTK_RELIEF_NORMAL + True + + + + False + False + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - + True - True - True - button4 - True - GTK_RELIEF_NORMAL - True + True + True + False + + + + True + Elim + True + elim + True + GTK_RELIEF_NORMAL + True + + + + False + False + + + + + + True + True + True + False + + + + True + ElimType + True + elimTy + True + GTK_RELIEF_NORMAL + True + + + + + False + False + 0 False - True + False - + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + Split + True + split + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + Left + True + left + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + Right + True + right + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + Exists + True + ∃ + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + - 5 + 0 False - True + False - + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + Reflexivity + True + refl + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + Symmetry + True + sym + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + Transitivity + True + trans + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + Assumption + True + assum + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + Search + True + search + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + Auto + True + auto + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + Cut + True + cut + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + True + Replace + True + repl + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + @@ -1464,4 +1902,123 @@ Copyright (C) 2004, + + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 0 + 0 + 0 + + + + + + 0 + True + True + + + + + + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 2619b9bb9..e565c03a7 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -127,6 +127,14 @@ let interpreter = let console = gui#console in new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console () + (** prompt the user for the textual input of a term and disambiguate it *) +let ask_term ?(title = "term input") ?(msg = "insert term") () = + match gui#askText ~title ~msg () with + | Some t -> + let (_, _, term) = disambiguator#disambiguateTerm (Stream.of_string t) in + Some term + | None -> None + let _ = gui#setQuitCallback quit; gui#setPhraseCallback interpreter#evalPhrase; @@ -155,7 +163,36 @@ let _ = | Some f -> gui#console#echo_error (sprintf "Don't know what to do with file: %s\nUnrecognized file format." - f))) + f))); + let tac_w_term name tac _ = + match ask_term ~title:name ~msg:("term for " ^ name) () with + | Some term -> (get_proof ())#apply_tactic (tac ~term) + | None -> () + in + let tac _ tac _ = (get_proof ())#apply_tactic tac in + let tbar = gui#toolbar in + ignore (tbar#introsButton#connect#clicked (tac "intros" (Tactics.intros ()))); + ignore (tbar#applyButton#connect#clicked (tac_w_term "apply" Tactics.apply)); + ignore (tbar#exactButton#connect#clicked (tac_w_term "exact" Tactics.exact)); + ignore (tbar#elimButton#connect#clicked (tac_w_term "elim" + Tactics.elim_intros_simpl)); + ignore (tbar#elimTypeButton#connect#clicked (tac_w_term "elim type" + Tactics.elim_type)); + ignore (tbar#splitButton#connect#clicked (tac "split" Tactics.split)); + ignore (tbar#leftButton#connect#clicked (tac "left" Tactics.left)); + ignore (tbar#rightButton#connect#clicked (tac "right" Tactics.right)); + ignore (tbar#existsButton#connect#clicked (tac "exists" Tactics.exists)); + ignore (tbar#reflexivityButton#connect#clicked (tac "reflexivity" + Tactics.reflexivity)); + ignore (tbar#symmetryButton#connect#clicked (tac "symmetry" + Tactics.symmetry)); + ignore (tbar#transitivityButton#connect#clicked (tac_w_term "transitivity" + Tactics.transitivity)); + ignore (tbar#assumptionButton#connect#clicked (tac "assumption" + Tactics.assumption)); + ignore (tbar#cutButton#connect#clicked (tac_w_term "cut" + (Tactics.cut ?mk_fresh_name_callback:None))); + ignore (tbar#autoButton#connect#clicked (tac "auto" (Tactics.auto ~dbd))) (** *) diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index cb7200391..95ae9648e 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -236,30 +236,102 @@ class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GBin.event_box (GtkBin.EventBox.cast (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata)) method toolBarEventBox = toolBarEventBox - val vbox1 = + val toolBarVBox = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox1" ~info:"GtkVBox" xmldata)) - method vbox1 = vbox1 - val vbuttonbox1 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"vbuttonbox1" ~info:"GtkVButtonBox" xmldata)) - method vbuttonbox1 = vbuttonbox1 - val button1 = + (Glade.get_widget_msg ~name:"ToolBarVBox" ~info:"GtkVBox" xmldata)) + method toolBarVBox = toolBarVBox + val toolbar2 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar2" ~info:"GtkToolbar" xmldata)) + method toolbar2 = toolbar2 + val introsButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"introsButton" ~info:"GtkButton" xmldata)) + method introsButton = introsButton + val applyButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"applyButton" ~info:"GtkButton" xmldata)) + method applyButton = applyButton + val exactButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"exactButton" ~info:"GtkButton" xmldata)) + method exactButton = exactButton + val toolbar3 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar3" ~info:"GtkToolbar" xmldata)) + method toolbar3 = toolbar3 + val elimButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"elimButton" ~info:"GtkButton" xmldata)) + method elimButton = elimButton + val elimTypeButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"elimTypeButton" ~info:"GtkButton" xmldata)) + method elimTypeButton = elimTypeButton + val toolbar4 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar4" ~info:"GtkToolbar" xmldata)) + method toolbar4 = toolbar4 + val splitButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"splitButton" ~info:"GtkButton" xmldata)) + method splitButton = splitButton + val leftButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"button1" ~info:"GtkButton" xmldata)) - method button1 = button1 - val button2 = + (Glade.get_widget_msg ~name:"leftButton" ~info:"GtkButton" xmldata)) + method leftButton = leftButton + val rightButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"button2" ~info:"GtkButton" xmldata)) - method button2 = button2 - val button3 = + (Glade.get_widget_msg ~name:"rightButton" ~info:"GtkButton" xmldata)) + method rightButton = rightButton + val existsButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"button3" ~info:"GtkButton" xmldata)) - method button3 = button3 - val button4 = + (Glade.get_widget_msg ~name:"existsButton" ~info:"GtkButton" xmldata)) + method existsButton = existsButton + val toolbar5 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar5" ~info:"GtkToolbar" xmldata)) + method toolbar5 = toolbar5 + val reflexivityButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"reflexivityButton" ~info:"GtkButton" xmldata)) + method reflexivityButton = reflexivityButton + val symmetryButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"symmetryButton" ~info:"GtkButton" xmldata)) + method symmetryButton = symmetryButton + val transitivityButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata)) + method transitivityButton = transitivityButton + val toolbar6 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata)) + method toolbar6 = toolbar6 + val assumptionButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata)) + method assumptionButton = assumptionButton + val searchButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"searchButton" ~info:"GtkButton" xmldata)) + method searchButton = searchButton + val autoButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata)) + method autoButton = autoButton + val toolbar7 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar7" ~info:"GtkToolbar" xmldata)) + method toolbar7 = toolbar7 + val cutButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"button4" ~info:"GtkButton" xmldata)) - method button4 = button4 + (Glade.get_widget_msg ~name:"cutButton" ~info:"GtkButton" xmldata)) + method cutButton = cutButton + val replaceButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"replaceButton" ~info:"GtkButton" xmldata)) + method replaceButton = replaceButton method reparent parent = toolBarEventBox#misc#reparent parent; toplevel#destroy () @@ -604,9 +676,57 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = toplevel#destroy () method check_widgets () = () end +class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"TextDialog" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) + method toplevel = toplevel + val textDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) + method textDialog = textDialog + val vbox5 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"vbox5" ~info:"GtkVBox" xmldata)) + method vbox5 = vbox5 + val hbuttonbox1 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"hbuttonbox1" ~info:"GtkHButtonBox" xmldata)) + method hbuttonbox1 = hbuttonbox1 + val textDialogCancelButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata)) + method textDialogCancelButton = textDialogCancelButton + val textDialogOkButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata)) + method textDialogOkButton = textDialogOkButton + val textDialogLabel = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata)) + method textDialogLabel = textDialogLabel + val scrolledwindow2 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"scrolledwindow2" ~info:"GtkScrolledWindow" xmldata)) + method scrolledwindow2 = scrolledwindow2 + val textDialogTextView = + new GText.view (GtkText.View.cast + (Glade.get_widget_msg ~name:"TextDialogTextView" ~info:"GtkTextView" xmldata)) + method textDialogTextView = textDialogTextView + method reparent parent = + vbox5#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end let check_all ?(show=false) () = ignore (GMain.Main.init ()); + let textDialog = new textDialog () in + if show then textDialog#toplevel#show (); + textDialog#check_widgets (); let scriptWin = new scriptWin () in if show then scriptWin#toplevel#show (); scriptWin#check_widgets (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 3c646b10c..d8e34fca3 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -137,28 +137,64 @@ class toolBarWin : ?autoconnect:bool -> unit -> object - val button1 : GButton.button - val button2 : GButton.button - val button3 : GButton.button - val button4 : GButton.button + val applyButton : GButton.button + val assumptionButton : GButton.button + val autoButton : GButton.button + val cutButton : GButton.button + val elimButton : GButton.button + val elimTypeButton : GButton.button + val exactButton : GButton.button + val existsButton : GButton.button + val introsButton : GButton.button + val leftButton : GButton.button + val reflexivityButton : GButton.button + val replaceButton : GButton.button + val rightButton : GButton.button + val searchButton : GButton.button + val splitButton : GButton.button + val symmetryButton : GButton.button val toolBarEventBox : GBin.event_box + val toolBarVBox : GPack.box val toolBarWin : GWindow.window + val toolbar2 : GButton.toolbar + val toolbar3 : GButton.toolbar + val toolbar4 : GButton.toolbar + val toolbar5 : GButton.toolbar + val toolbar6 : GButton.toolbar + val toolbar7 : GButton.toolbar val toplevel : GWindow.window - val vbox1 : GPack.box - val vbuttonbox1 : GPack.button_box + val transitivityButton : GButton.button val xml : Glade.glade_xml Gtk.obj + method applyButton : GButton.button + method assumptionButton : GButton.button + method autoButton : GButton.button method bind : name:string -> callback:(unit -> unit) -> unit - method button1 : GButton.button - method button2 : GButton.button - method button3 : GButton.button - method button4 : GButton.button method check_widgets : unit -> unit + method cutButton : GButton.button + method elimButton : GButton.button + method elimTypeButton : GButton.button + method exactButton : GButton.button + method existsButton : GButton.button + method introsButton : GButton.button + method leftButton : GButton.button + method reflexivityButton : GButton.button method reparent : GObj.widget -> unit + method replaceButton : GButton.button + method rightButton : GButton.button + method searchButton : GButton.button + method splitButton : GButton.button + method symmetryButton : GButton.button method toolBarEventBox : GBin.event_box + method toolBarVBox : GPack.box method toolBarWin : GWindow.window + method toolbar2 : GButton.toolbar + method toolbar3 : GButton.toolbar + method toolbar4 : GButton.toolbar + method toolbar5 : GButton.toolbar + method toolbar6 : GButton.toolbar + method toolbar7 : GButton.toolbar method toplevel : GWindow.window - method vbox1 : GPack.box - method vbuttonbox1 : GPack.button_box + method transitivityButton : GButton.button method xml : Glade.glade_xml Gtk.obj end class confirmationDialog : @@ -383,4 +419,34 @@ class scriptWin : method vbox4 : GPack.box method xml : Glade.glade_xml Gtk.obj end +class textDialog : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val hbuttonbox1 : GPack.button_box + val scrolledwindow2 : GBin.scrolled_window + val textDialog : GWindow.dialog_any + val textDialogCancelButton : GButton.button + val textDialogLabel : GMisc.label + val textDialogOkButton : GButton.button + val textDialogTextView : GText.view + val toplevel : GWindow.dialog_any + val vbox5 : GPack.box + val xml : Glade.glade_xml Gtk.obj + method bind : name:string -> callback:(unit -> unit) -> unit + method check_widgets : unit -> unit + method hbuttonbox1 : GPack.button_box + method reparent : GObj.widget -> unit + method scrolledwindow2 : GBin.scrolled_window + method textDialog : GWindow.dialog_any + method textDialogCancelButton : GButton.button + method textDialogLabel : GMisc.label + method textDialogOkButton : GButton.button + method textDialogTextView : GText.view + method toplevel : GWindow.dialog_any + method vbox5 : GPack.box + method xml : Glade.glade_xml Gtk.obj + end val check_all : ?show:bool -> unit -> unit diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 6b70a498f..d50a2f319 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -164,6 +164,26 @@ class gui file = GtkThread.main (); chosen_file + method askText ?(title = "") ?(msg = "") () = + let dialog = new textDialog () in + dialog#textDialog#set_title title; + dialog#textDialogLabel#set_label msg; + let text = ref None in + let return v = + text := v; + dialog#textDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#textDialog#event#connect#delete (fun _ -> true)); + ignore (dialog#textDialogCancelButton#connect#clicked (fun _ -> + return None)); + ignore (dialog#textDialogOkButton#connect#clicked (fun _ -> + let text = dialog#textDialogTextView#buffer#get_text () in + return (Some text))); + dialog#textDialog#show (); + GtkThread.main (); + !text + end let instance = diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index a185aaf74..a74403fdb 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -63,6 +63,7 @@ class gui : method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog method chooseFile: unit -> string option + method askText: ?title:string -> ?msg:string -> unit -> string option end diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 17a055174..d5ca65d22 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -188,28 +188,26 @@ class proofState | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *) PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () - | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac - | TacticAst.Assumption -> VariousTactics.assumption_tac - | TacticAst.Contradiction -> NegationTactics.contradiction_tac - | TacticAst.Exists -> IntroductionTactics.exists_tac - | TacticAst.Fourier -> FourierR.fourier_tac - | TacticAst.Left -> IntroductionTactics.left_tac - | TacticAst.Right -> IntroductionTactics.right_tac - | TacticAst.Ring -> Ring.ring_tac - | TacticAst.Split -> IntroductionTactics.split_tac - | TacticAst.Symmetry -> EqualityTactics.symmetry_tac - | TacticAst.Transitivity term -> - EqualityTactics.transitivity_tac (disambiguate term) - | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term) - | TacticAst.Absurd term -> NegationTactics.absurd_tac (disambiguate term) - | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term) - | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term) + | TacticAst.Reflexivity -> Tactics.reflexivity + | TacticAst.Assumption -> Tactics.assumption + | TacticAst.Contradiction -> Tactics.contradiction + | TacticAst.Exists -> Tactics.exists + | TacticAst.Fourier -> Tactics.fourier + | TacticAst.Left -> Tactics.left + | TacticAst.Right -> Tactics.right + | TacticAst.Ring -> Tactics.ring + | TacticAst.Split -> Tactics.split + | TacticAst.Symmetry -> Tactics.symmetry + | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term) + | TacticAst.Apply term -> Tactics.apply (disambiguate term) + | TacticAst.Absurd term -> Tactics.absurd (disambiguate term) + | TacticAst.Exact term -> Tactics.exact (disambiguate term) + | TacticAst.Cut term -> Tactics.cut (disambiguate term) | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *) - PrimitiveTactics.elim_intros_simpl_tac (disambiguate term) - | TacticAst.ElimType term -> - EliminationTactics.elim_type_tac (disambiguate term) + Tactics.elim_intros_simpl (disambiguate term) + | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term) | TacticAst.Replace (what, with_what) -> - EqualityTactics.replace_tac ~what:(disambiguate what) + Tactics.replace ~what:(disambiguate what) ~with_what:(disambiguate with_what) (* (* TODO Zack a lot more of tactics to be implemented here ... *) -- 2.39.2