diff --git a/CHANGELOG.md b/CHANGELOG.md index 7c2fbc5ad01d237511d268de668a4ec22ac937a9..ff053daedffc41896b185471dd8d67870fe36640 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,8 +14,8 @@ Changes in and extensions of the theory: Changes in Coq: * Rename `timelessP` -> `timeless` (projection of the `Timeless` class) -* 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 functionnal +* 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. ## Iris 3.1.0 (released 2017-12-19)