From 6b9bcc13c64563dfcb66d9bf4218a1d2fd9776c2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 May 2023 11:55:59 +0200
Subject: [PATCH] changelog

---
 CHANGELOG.md | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 83c26d5dd..71e953e1b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,13 @@ lemma.
 
 Coq 8.13 is no longer supported.
 
+**Changes in `prelude`:**
+
+* Re-export `stdpp.options` from `iris.prelude.options`. This enables 'light'
+  name mangling, which prefixes auto-generated names with `__`. This only
+  affects developments that explicitly opt-in to following the Iris
+  configuration by importing `iris.prelude.options`.
+
 **Changes in `algebra`:**
 
 * Add (basic) support for `gset` and `gset_disj` cameras to `set_solver`.
@@ -90,6 +97,9 @@ Coq 8.13 is no longer supported.
 
 **Changes in `base_logic`:**
 
+* Add `mono_Z` library for monotone non-negative integers.
+  (This has exactly the same lemmas as `mono_nat`. It is useful in cases
+  where one wants to avoid `nat` entirely and use `Z` throughout.)
 * Add `IsExcept0` instance for invariants, allowing you to remove laters of
   timeless hypotheses when proving an invariant (without an update).
 * Make `uPred.unseal` tactic more robust by using types to unfold the right
@@ -108,12 +118,6 @@ Coq 8.13 is no longer supported.
   postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`.
 * Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim).
 
-**Changes in `base_logic`:**
-
-* Add `mono_Z` library for monotone non-negative integers.
-  (This has exactly the same lemmas as `mono_nat`. It is useful in cases
-  where one wants to avoid `nat` entirely and use `Z` throughout.)
-
 **LaTeX changes:**
 
 - Rename `\Alloc` to `\AllocN` and `\Ref` to `\Alloc` for better consistency
-- 
GitLab