From c8a79f5aa9704d15d10aa6aaa4cfaadcd4ae5a1f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 24 Aug 2019 20:41:14 +0200
Subject: [PATCH] Add changelog entry.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 35ca2308c..1345249ad 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -164,6 +164,8 @@ Changes in Coq:
 * Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`,
   `Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`,
   `cmra_morphism_core`.
+* Rename lemmas `fupd_big_sep{L,M,S,MS}` into `big_sep{L,M,S,MS}_fupd` to be
+  consistent with other such big op lemmas. Also add such lemmas for `bupd`.
 * Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also
   rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into
   `-d>`. The renaming can be automatically done using the following script (on
-- 
GitLab