Commit 4285f31a authored by Ralf Jung's avatar Ralf Jung

add disjointness change to changelog

parent fd912b5c
...@@ -18,6 +18,7 @@ Changes in Coq: ...@@ -18,6 +18,7 @@ Changes in Coq:
* Rename some things and change notation: * Rename some things and change notation:
- The unit of a camera: `empty` -> `unit`, `∅` -> `ε` - The unit of a camera: `empty` -> `unit`, `∅` -> `ε`
- Disjointness: `⊥` -> `##`
- A proof mode type class `IntoOp` -> `IsOp` - A proof mode type class `IntoOp` -> `IsOp`
- OFEs with all elements being discrete: `Discrete` -> `OfeDiscrete` - OFEs with all elements being discrete: `Discrete` -> `OfeDiscrete`
- OFE elements whose equality is discrete: `Timeless` -> `Discrete` - OFE elements whose equality is discrete: `Timeless` -> `Discrete`
......
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