From 63a0ea9ebb1dc9e2dfe6fa0b1fd55affb4f06c9f Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Fri, 24 May 2019 10:13:59 +0200
Subject: [PATCH] Add renaming for to CHANGELOG
---
CHANGELOG.md | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index d295f277e..0c3460025 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -119,6 +119,12 @@ 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.
+* 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`.
+ - Use `auth_auth` and `auth_frag` for the injections into authoritative
+ elements and non-authoritative elements respectively.
+ - Lemmas for the projections and injections are renamed accordingly.
## Iris 3.1.0 (released 2017-12-19)
--
GitLab