From 02b65ee9dc3da8a7ef413c438d917d5d2a57bffb Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Fri, 24 May 2019 15:10:53 +0200
Subject: [PATCH] More rename

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4029e7119..5ab682fcd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -125,6 +125,11 @@ Changes in Coq:
   - 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.
+    For examples:
+    + `authoritative_validN` → `auth_auth_proj_validN`
+    + `auth_own_validN` → `auth_frag_proj_validN`
+    + `auth_auth_valid` was not renamed because it was already used for the
+      authoritative injection.
   - `auth_both_valid` → `auth_both_valid_2`
   - `auth_valid_discrete_2` → `auth_both_valid`
 
-- 
GitLab