From 36c0816cccdea4c5aaf9e95a372248e432b5a69c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Oct 2017 10:53:20 +0200
Subject: [PATCH] expand changelog

---
 CHANGELOG.md | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 94502beb7..16efc41bc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -16,7 +16,18 @@ Changes in Coq:
 
 * Some things got renamed and notation changed:
   - The unit of a CMRA: empty -> unit, ∅ -> ε
-  - IntoOp -> IsOp
+  - ?: IntoOp -> IsOp
+  - OFEs with all elements being discrete: Discrete -> OfeDiscrete
+  - OFE elements whose equality is discrete: Timeless -> Discrete
+  - Timeless propositions: TimelessP -> Timeless
+  - Camera elements such that `core x = x`: Persistent -> CoreId
+  - Persistent propositions: PersistentP -> Persistent
+  - The persistent modality: always -> persistently
+  - Consistently SnakeCase identifiers: CMRAMixin -> CmraMixin, CMRAT -> CmraT,
+    CMRATotal -> CmraTotal, CMRAMorphism -> CmraMorphism,
+    UCMRAMixin -> UcmraMixin, UCMRAT -> UcmraT, DRAMixin -> DraMixin,
+    DRAT -> DraT, STS -> Sts
+  - ? more
 * Fix a bunch of consistency issues in the proof mode, and make it overall more
   usable.  In particular:
   - All proof mode tactics start the proof mode if necessary; iStartProof is no
-- 
GitLab