Commit 1c2ea26d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add Changelog entry.

parent 85245d48
......@@ -90,7 +90,9 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
+ The version of big operations over lists was redefined so that it enjoys
more definitional equalities.
* Various improvements to `solve_ndisj`.
* Improve handling of pure (non-state-dependent) reductions in heap_lang.
* Some extensions/improvements of heap_lang:
- Improve handling of pure (non-state-dependent) reductions.
- Add fetch-and-add (`FAA`) operation.
* Use `Hint Mode` to prevent Coq from making arbitrary guesses in the presence
of evars, which often led to divergence. There are a few places where type
annotations are now needed.
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