From 1d11aac6e98aa89d86d32f5109774193f3575225 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 24 Jun 2019 09:41:44 +0200
Subject: [PATCH] more consistent order and format for CHANGELOG
---
CHANGELOG.md | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 43b69064d..27a81b79d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -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)
--
GitLab