From d4441722649a053fbabccbac3cd2c17e7e55dedf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 20 Oct 2020 17:09:18 +0200
Subject: [PATCH] changelog

---
 CHANGELOG.md                  | 7 +++++++
 theories/base_logic/algebra.v | 1 -
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 079989202..1d11d3930 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,6 +46,9 @@ With this release, we dropped support for Coq 8.9.
   key, including support for persistent read-only ownership through `dfrac`.
   See `theories/algebra/lib/gmap_view.v` for further information.
   NOTE: The API surface for `gmap_view` is experimental and subject to change.
+* Move the `*_validI` and `*_equivI` lemmas to a new module, `base_logic.algebra`.
+  That module is exported by `base_logic.base_logic` so it should usually be
+  available everywhere without further changes.
 
 **Changes in `proofmode`:**
 
@@ -96,6 +99,10 @@ With this release, we dropped support for Coq 8.9.
   the state interpretation of WP and since `_ctx` is elsewhere used as a suffix
   indicating "this is a persistent assumption that clients should always have in
   their context". Likewise, rename `proph_map_ctx` to `proph_map_interp`.
+* Move `uPred.prod_validI`, `uPred.option_validI`, and
+  `uPred.discrete_fun_validI` to the new `base_logic.algebra` module. That
+  module is exported by `base_logic.base_logic` so these names are now usually
+  available everywhere, and no longer inside the `uPred` module.
 
 **Changes in `program_logic`:**
 
diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index 6c86be60b..d185f4a17 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -196,7 +196,6 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
-  (** Internalized properties *)
   Lemma auth_auth_frac_validI q a : ✓ (●{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
   Proof.
     apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].
-- 
GitLab