diff options
| author | Jim Fehrle | 2021-01-19 11:19:33 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-01-20 12:10:08 -0800 |
| commit | cd17f9bfad72fb8f8da486facd75ff8ceecebd24 (patch) | |
| tree | 0c7f0f876b529f7b13ce707edc252d10627307db /doc/changelog | |
| parent | 071c50e9c2755e93766e5fb047b0a9065934e8fe (diff) | |
Remove double induction tactic
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/04-tactics/13762-remove_double_induction.rst | 9 |
1 files changed, 9 insertions, 0 deletions
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). |