Commit 1d11aac6 authored by Ralf Jung's avatar Ralf Jung

more consistent order and format for CHANGELOG

parent 43fb8444
......@@ -131,6 +131,8 @@ Changes in Coq:
authoritative elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`. As a
consequence, `auth` is no longer a COFE and does not preserve Leibniz
equality.
* Add a COFE construction (and functor) on dependent pairs `sigTO`, dual to
`discrete_funO`.
* Rename in `auth`:
- Use `auth_auth_proj`/`auth_frag_proj` for the projections of `auth`:
`authoritative``auth_auth_proj` and `auth_own``auth_frag_proj`.
......@@ -208,8 +210,6 @@ s/\bgnameC/gnameO/g;
s/\bcoPset\_disjC/coPset\_disjO/g;
' $(find theories -name "*.v")
```
- Add a COFE construction (and functor) on dependent pairs `sigTO`, dual to
`discrete_funO`.
## Iris 3.1.0 (released 2017-12-19)
......
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