diff --git a/CHANGELOG.md b/CHANGELOG.md index 1a2e928df04bd384a2f5bd76dc3a46bb03963026..c59f48658996dfa3ee008f19f357b54b002e2421 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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