Remove the Tactic menu from CoqIDE.

Partial fix of #11219: CoqIDE tactics and templates menus are out of sync.

Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>

6 files changed, 2 insertions, 218 deletions

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index bfd99e7ce3..5b9ea17ba7 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -228,198 +228,3 @@ let state_preserving = [
   "Test Printing Wildcard";
 
 ]
-
-
-let tactics =
-  [
-    [
-      "abstract";
-      "absurd";
-      "apply";
-      "apply __ with";
-      "assert";
-      "assert (__:__)";
-      "assert (__:=__)";
-      "assumption";
-      "auto";
-      "auto with";
-      "autorewrite";
-    ];
-
-   [
-     "case";
-     "case __ with";
-     "casetype";
-     "cbv";
-     "cbv in";
-     "change";
-     "change __ in";
-     "clear";
-     "clearbody";
-     "cofix";
-     "compare";
-     "compute";
-     "compute in";
-     "congruence";
-     "constructor";
-     "constructor __ with";
-     "contradiction";
-     "cut";
-     "cutrewrite";
-   ];
-
-   [
-     "decide equality";
-     "decompose";
-     "decompose record";
-     "decompose sum";
-     "dependent inversion";
-     "dependent inversion __ with";
-     "dependent inversion__clear";
-     "dependent inversion__clear __ with";
-     "dependent rewrite ->";
-     "dependent rewrite <-";
-     "destruct";
-     "discriminate";
-     "do";
-     "double induction";
-   ];
-
-   [
-     "eapply";
-     "eauto";
-     "eauto with";
-     "eexact";
-     "elim";
-     "elim __ using";
-     "elim __ with";
-     "elimtype";
-     "exact";
-     "exists";
-   ];
-
-   [
-     "fail";
-     "field";
-     "first";
-     "firstorder";
-     "firstorder using";
-     "firstorder with";
-     "fix";
-     "fix __ with";
-     "fold";
-     "fold __ in";
-     "functional induction";
-   ];
-
-   [
-     "generalize";
-     "generalize dependent";
-   ];
-
-   [
-     "hnf";
-   ];
-
-   [
-     "idtac";
-     "induction";
-     "info";
-     "injection";
-     "instantiate (__:=__)";
-     "intro";
-     "intro after";
-     "intro __ after";
-     "intros";
-     "intros until";
-     "intuition";
-     "inversion";
-     "inversion __ in";
-     "inversion __ using";
-     "inversion __ using __ in";
-     "inversion__clear";
-     "inversion__clear __ in";
-   ];
-
-   [
-     "jp <n>";
-     "jp";
-   ];
-
-   [
-     "lapply";
-     "lazy";
-     "lazy in";
-     "left";
-   ];
-
-   [
-     "move __ after";
-   ];
-
-   [
-     "omega";
-   ];
-
-   [
-     "pattern";
-     "pose";
-     "pose __:=__)";
-     "progress";
-   ];
-
-   [
-     "quote";
-   ];
-
-   [
-     "red";
-     "red in";
-     "refine";
-     "reflexivity";
-     "rename __ into";
-     "repeat";
-     "replace __ with";
-     "rewrite";
-     "rewrite __ in";
-     "rewrite <-";
-     "rewrite <- __ in";
-     "right";
-     "ring";
-   ];
-
-   [
-     "set";
-     "set (__:=__)";
-     "setoid__replace";
-     "setoid__rewrite";
-     "simpl";
-     "simpl __ in";
-     "simple destruct";
-     "simple induction";
-     "simple inversion";
-     "simplify__eq";
-     "solve";
-     "split";
-(*     "split__Rabs";
-     "split__Rmult";
-*)
-     "subst";
-     "symmetry";
-     "symmetry in";
-   ];
-
-   [
-     "tauto";
-     "transitivity";
-     "trivial";
-     "try";
-   ];
-
-   [
-     "unfold";
-     "unfold __ in";
-   ];
-]
-
-
diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli
index 5f8ce30901..c8c11f77af 100644
--- a/ide/coq_commands.mli
+++ b/ide/coq_commands.mli
@@ -8,6 +8,5 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val tactics : string list list
 val commands : string list list
 val state_preserving : string list
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 918c196968..a519577c2c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -977,7 +977,6 @@ let build_ui () =
   let view_menu = GAction.action_group ~name:"View" () in
   let export_menu = GAction.action_group ~name:"Export" () in
   let navigation_menu = GAction.action_group ~name:"Navigation" () in
-  let tactics_menu = GAction.action_group ~name:"Tactics" () in
   let templates_menu = GAction.action_group ~name:"Templates" () in
   let tools_menu = GAction.action_group ~name:"Tools" () in
   let queries_menu = GAction.action_group ~name:"Queries" () in
@@ -985,7 +984,7 @@ let build_ui () =
   let windows_menu = GAction.action_group ~name:"Windows" () in
   let help_menu = GAction.action_group ~name:"Help" () in
   let all_menus = [
-    file_menu; edit_menu; view_menu; export_menu; navigation_menu; tactics_menu;
+    file_menu; edit_menu; view_menu; export_menu; navigation_menu;
     templates_menu; tools_menu; queries_menu; compile_menu; windows_menu;
     help_menu; ] in
 
@@ -1121,11 +1120,6 @@ let build_ui () =
     ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f");
   ] end;
 
-  menu tactics_menu [
-    item "Tactics" ~label:"_Tactics";
-  ];
-  alpha_items tactics_menu "Tactic" Coq_commands.tactics;
-
   menu templates_menu [
     item "Templates" ~label:"Te_mplates";
     template_item ("Lemma new_lemma : .\nProof.\n\nQed.\n", 6,9, "J");
@@ -1209,7 +1203,6 @@ let build_ui () =
   Coqide_ui.ui_m#insert_action_group edit_menu 0;
   Coqide_ui.ui_m#insert_action_group view_menu 0;
   Coqide_ui.ui_m#insert_action_group navigation_menu 0;
-  Coqide_ui.ui_m#insert_action_group tactics_menu 0;
   Coqide_ui.ui_m#insert_action_group templates_menu 0;
   Coqide_ui.ui_m#insert_action_group tools_menu 0;
   Coqide_ui.ui_m#insert_action_group queries_menu 0;
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index f056af6703..3793c4be21 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -100,9 +100,6 @@ let init () =
 \n    <menuitem action='Previous' />\
 \n    <menuitem action='Next' />\
 \n  </menu>\
-\n  <menu action='Tactics'>\
-\n    %s\
-\n  </menu>\
 \n  <menu action='Templates'>\
 \n    <menuitem action='Lemma' />\
 \n    <menuitem action='Theorem' />\
@@ -165,7 +162,6 @@ let init () =
 \n</toolbar>\
 \n</ui>"
     (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
-    (Buffer.contents (list_items "Tactic" Coq_commands.tactics))
     (Buffer.contents (list_items "Template" Coq_commands.commands))
     (Buffer.contents (list_queries "User-Query" Preferences.user_queries#get))
  in
diff --git a/ide/preferences.ml b/ide/preferences.ml
index d3cf08e90e..af1759b0bb 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -331,10 +331,6 @@ let modifier_for_navigation =
 let modifier_for_templates =
   new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
 
-let modifier_for_tactics =
-  new preference ~name:["modifier_for_tactics"]
-    ~init:(select_arch "<Control><Alt>" "<Control><Primary>") ~repr:Repr.(string)
-
 let modifier_for_display =
   new preference ~name:["modifier_for_display"]
     ~init:(select_arch "<Alt><Shift>" "<Primary><Shift>")~repr:Repr.(string)
@@ -347,7 +343,6 @@ let attach_modifiers_callback () =
   (* To be done after the preferences are loaded *)
   let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/" in
   let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/" in
-  let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/" in
   let _ = attach_modifiers modifier_for_display "<Actions>/View/" in
   let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" in
   ()
@@ -951,9 +946,6 @@ let configure ?(apply=(fun () -> ())) parent =
       (string_of_project_behavior read_project#get)
   in
   let project_file_name = pstring "Default name for project file" project_file_name in
-  let modifier_for_tactics =
-    pmodifiers "Global change of modifiers for Tactics Menu" modifier_for_tactics
-  in
   let modifier_for_templates =
     pmodifiers "Global change of modifiers for Templates Menu" modifier_for_templates
   in
@@ -1056,7 +1048,7 @@ let configure ?(apply=(fun () -> ())) parent =
              [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
               cmd_print;cmd_editor;cmd_browse]);
      Section("Shortcuts", Some `PREFERENCES,
-             [modifiers_valid; modifier_for_tactics;
+             [modifiers_valid;
         modifier_for_templates; modifier_for_display; modifier_for_navigation;
         modifier_for_queries (*; user_queries *)]);
      Section("Misc", Some `ADD,
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 7b43079b4f..754f15c575 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -71,7 +71,6 @@ val automatic_tactics : string list preference
 val cmd_print : string preference
 val modifier_for_navigation : string preference
 val modifier_for_templates : string preference
-val modifier_for_tactics : string preference
 val modifier_for_display : string preference
 val modifier_for_queries : string preference
 val modifiers_valid : string preference