From 044f76cf32080f0a56309544e5335e44f89725b4 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 28 May 2020 15:25:14 -0700
Subject: Remove info tactic, deprecated in 8.5

---
 doc/changelog/04-tactics/12423-rm-info.rst | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 doc/changelog/04-tactics/12423-rm-info.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/12423-rm-info.rst b/doc/changelog/04-tactics/12423-rm-info.rst
new file mode 100644
index 0000000000..bf20453e6b
--- /dev/null
+++ b/doc/changelog/04-tactics/12423-rm-info.rst
@@ -0,0 +1,2 @@
+- **Removed:** Removed info tactic that was deprecated in 8.5.
+  (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle).
-- 
cgit v1.2.3