From c0ebfd453f82cbf9965ccba621aa68edde35ea72 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 Jan 2020 12:29:31 +0100 Subject: 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 --- doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst (limited to 'doc') diff --git a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst new file mode 100644 index 0000000000..6294cdb24a --- /dev/null +++ b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst @@ -0,0 +1,4 @@ +- **Removed:** + Removed the "Tactic" menu from CoqIDE which had been unmaintained for a number of years + (`#11414 `_, + by Pierre-Marie Pédrot). -- cgit v1.2.3