Commit 2e873a3a authored by Robbert Krebbers's avatar Robbert Krebbers

Add note about iIntros/iAlways to CHANGELOG.

parent 92c7d5d0
......@@ -65,6 +65,12 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
mode.
- Many missing type class instances for distributing connectives have been
defined.
- The tactics `iIntros (?)` and `iIntros "!#"` (i.e. `iAlways`) are now
implemented using type classes. That way, they are more generic, e.g.
`iIntros (?)` also works when the universal quantifier is below a modality,
and `iAlways` also works for the plainness modality. A breaking change,
however, is that these tactics now no longer work when the universal
quantifier or modality is behind a type class opaque definition.
* The generic `fill` operation of the `ectxi_language` construct has been
defined in terms of a left fold instead of a right fold. This gives rise to
more definitional equalities.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment