Commit aa6ecfbb authored by Ralf Jung's avatar Ralf Jung
Browse files


parent 24656b41
......@@ -36,6 +36,8 @@ Changes in Coq:
* The `iInv` tactic can now be used without the second argument (the name for
the closing update). It will then instead add the obligation to close the
invariant to the goal.
* Added support for defining derived connectives involving n-ary binders using
* Improved pretty-printing of Iris connectives (in particular WP and fancy
updates) when Coq has to line-wrap the output.
* Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
Supports Markdown
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