From b059329d76eab941bf206de5ad3eef5e288f6391 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 3 Oct 2020 11:44:49 +0200
Subject: [PATCH] expand auth changelog
---
CHANGELOG.md | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7d7552168..735ea509d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,8 +33,9 @@ With this release, we dropped support for Coq 8.9.
only way to construct elements of `auth` is via the elements `â—{q} a` and
`â—¯ b`. The constructor `Auth`, and the projections `auth_auth_proj` and
`auth_frag_proj` no longer exist. Lemmas that referred to these constructors
- have been removed, in particular, `auth_included`, `auth_valid_discrete`,
- and `auth_both_op`.
+ have been removed, in particular: `auth_equivI`, `auth_validI`,
+ `auth_included`, `auth_valid_discrete`, and `auth_both_op`. For validity, use
+ `auth_auth_valid*`, `auth_frag_valid*`, or `auth_both_valid*` instead.
**Changes in `proofmode`:**
--
GitLab