Skip to content
Snippets Groups Projects
Commit 8f1ed633 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak changelog for `persistently_True`.

parent 30df4002
No related branches found
No related tags found
No related merge requests found
......@@ -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`:**
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment