From 4f00de71c5091c6bc4072ceeedfc52a4f0a2d8b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org>
Date: Wed, 26 Feb 2020 22:26:22 +0100
Subject: [PATCH] Changelog entry
---
CHANGELOG.md | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index f4532cf3..adae4198 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,13 @@ API-breaking change is listed.
- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma
`list_to_vec_to_list` for the converse.
- Add `Countable` instance for `vec`.
+- Introduce `destruct_or{?,!}` to repeatedly destruct disjunctions in
+ assumptions. The tactic can also be provided an explicit assumption name;
+ `destruct_and{?,!}` has been generalized accordingly and now can also be
+ provided an explicit assumption name.
+ Slight breaking change: `destruct_and` no longer handle `False`;
+ `destruct_or` now handles `False` while `destruct_and` handles `True`,
+ as the respective units of disjunction and conjunction.
## std++ 1.2.1 (released 2019-08-29)
--
GitLab