Commit cbbb2896 authored by Ralf Jung's avatar Ralf Jung

edit changelog

parent dcdbcec7
......@@ -31,8 +31,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
* 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
1. Coq's "new" unification algorithm (the one in `refine`, not the "old" one
in `apply`) 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
......
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