From cd17f9bfad72fb8f8da486facd75ff8ceecebd24 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 19 Jan 2021 11:19:33 -0800
Subject: Remove double induction tactic

---
 doc/changelog/04-tactics/13762-remove_double_induction.rst | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 doc/changelog/04-tactics/13762-remove_double_induction.rst

(limited to 'doc/changelog')

diff --git a/doc/changelog/04-tactics/13762-remove_double_induction.rst b/doc/changelog/04-tactics/13762-remove_double_induction.rst
new file mode 100644
index 0000000000..4ea54a1ab6
--- /dev/null
+++ b/doc/changelog/04-tactics/13762-remove_double_induction.rst
@@ -0,0 +1,9 @@
+- **Removed:**
+  double induction tactic.  Replace :n:`double induction @ident @ident`
+  with :n:`induction @ident; induction @ident` (or
+  :n:`induction @ident ; destruct @ident` depending on the exact needs).
+  Replace :n:`double induction @natural__1 @natural__2` with
+  :n:`induction @natural__1; induction natural__3` where :n:`natural__3` is the result
+  of :n:`natural__2 - natural__1`
+  (`#13762 <https://github.com/coq/coq/pull/13762>`_,
+  by Jim Fehrle).
-- 
cgit v1.2.3