Commit 618ad0f9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent f133c8cd
......@@ -25,6 +25,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
Coq goal `big star of context ⊢ proof mode goal`.
* Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s.
Introduce `iProp` for the `Type` carrier of `iPropO`.
* Move derived camera constructions (`frac_auth` and `ufrac_auth`) to the folder
* Add derived camera construction `excl_auth A` for `auth (option (excl A))`.
## 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