Commit be5fe2c5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Update changelog.

parent ad308b56
......@@ -17,6 +17,11 @@ Changes in Coq:
* The CMRA axiom `cmra_extend` is now stated in `Type`, using `sigT` instead of
in `Prop` using `exists`. This makes it possible to define the function space
CMRA even for an infinite domain.
* Rename proof mode type classes for laters:
- `IntoLaterN``MaybeIntoLaterN` (this one _may_ strip a later)
- `IntoLaterN'``IntoLaterN` (this one _should_ strip a later)
- `IntoLaterNEnv``MaybeIntoLaterNEnv`
- `IntoLaterNEnvs``MaybeIntoLaterNEnvs`
## Iris 3.1.0 (released 2017-12-19)
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