Commit c23b13ee authored by Robbert Krebbers's avatar Robbert Krebbers

CHANGELOG for !329

parent d1787db2
......@@ -28,6 +28,16 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Move derived camera constructions (`frac_auth` and `ufrac_auth`) to the folder
`algebra/lib`.
* Add derived camera construction `excl_auth A` for `auth (option (excl A))`.
* Make use of `notypeclasses refine` in the implementation of `iPoseProof` and
`iAssumption`, see https://gitlab.mpi-sws.org/iris/iris/merge_requests/329
This has two consequences:
1. Coq's new unification algorithm is used more often by the proof mode
tactics
2. TC constraints are solved eagerly, see https://github.com/coq/coq/issues/6583.
In order to port your development, it is often needed to instantiate evars
explicitly (since TC search is performed less eagerly), and in few cases it is
needed to unfold definitions explicitly (due to new unification algorithm
behaving differently).
## Iris 3.2.0 (released 2019-08-29)
......
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