From 8341b39b800ff75a3a974486e4087100370a9a52 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 30 Sep 2020 21:11:49 +0200
Subject: [PATCH] CHANGELOG.
---
CHANGELOG.md | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2092181be..7d7552168 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -25,6 +25,16 @@ With this release, we dropped support for Coq 8.9.
* Rename `auth_both_valid` to `auth_both_valid_discrete` and
`auth_both_frac_valid` to `auth_both_frac_valid_discrete`. The old name is
used for new, stronger lemmas that do not assume discreteness.
+* Add the view camera `view`, which generalizes the authoritative camera
+ `auth` by being parameterized by a relation that relates the authoritative
+ element with the fragments.
+* Redefine the authoritative camera in terms of the view camera. As part of this
+ change, we have removed lemmas that leaked implementation details. Hence, the
+ 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`.
**Changes in `proofmode`:**
--
GitLab