Commit feccb48c authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents 2038efcb 94446fec
...@@ -27,7 +27,8 @@ Changes in and extensions of the theory: ...@@ -27,7 +27,8 @@ Changes in and extensions of the theory:
Changes in Coq: Changes in Coq:
* Move the `prelude` folder to its own project: std++ * Move the `prelude` folder to its own project:
[coq-std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
* Some extensions/improvements of heap_lang: * Some extensions/improvements of heap_lang:
- Improve handling of pure (non-state-dependent) reductions. - Improve handling of pure (non-state-dependent) reductions.
- Add fetch-and-add (`FAA`) operation. - Add fetch-and-add (`FAA`) operation.
...@@ -110,8 +111,8 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret ...@@ -110,8 +111,8 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
setup Iris for your language. setup Iris for your language.
* Restore the original, stronger notion of atomicity alongside the weaker * Restore the original, stronger notion of atomicity alongside the weaker
notion. These are `Atomic a e` where the stuckness bit `s` indicates whether notion. These are `Atomic a e` where the stuckness bit `s` indicates whether
expression `e` is weakly (`a = WeaklyAtomic`) or strongly (`a = expression `e` is weakly (`a = WeaklyAtomic`) or strongly
StronglyAtomic`) atomic. (`a = StronglyAtomic`) atomic.
* Various improvements to `solve_ndisj`. * Various improvements to `solve_ndisj`.
* Use `Hint Mode` to prevent Coq from making arbitrary guesses in the presence * 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 of evars, which often led to divergence. There are a few places where type
......
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