diff --git a/CHANGELOG.md b/CHANGELOG.md index 7747ffdaedb30b08d970e91af3b2dc9cc4bfbb9b..92bfbe9eb9a602dbe39d8b20f1a65fb67df5f07e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -47,7 +47,8 @@ Coq 8.13 is no longer supported. * Add compatibility lemmas for `big_sepL <-> big_sepL2`, `big_sepM <-> big_sepM2` with list/maps of pairs; and `big_sepM <-> big_sepL` via `list_to_map` and `map_to_list`. (by Dorian Lesbre). -- Make `persistently_True` a bi-entailment. +- Make `persistently_True` a bi-entailment; this changes the default `rewrite` + direction. - Make `BiLaterContractive` a class instead of a notation. **Changes in `proofmode`:**