From 1f93e2d067fab67c465b42a67fc2b947bc0e90eb Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 20 Jul 2022 17:23:56 -0500
Subject: [PATCH] Remove unused Qp argument to dfrac_valid_discarded

---
 CHANGELOG.md         | 1 +
 iris/algebra/dfrac.v | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7334ae546..73255a411 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,6 +73,7 @@ lemma.
   and `saved_pred_own`, so they can be updated. The previous persistent versions
   can be recovered with the fraction `DfracDiscarded`. Allocation lemmas now take
   a `dq` parameter to define the initial fraction.
+* Remove an unused fraction argument to `dfrac_valid_discarded`.
 
 **Changes in `program_logic`:**
 
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 30969cbba..3511d31b6 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -173,7 +173,7 @@ Section dfrac.
   Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
   Proof. rewrite comm. apply dfrac_valid_own_r. Qed.
 
-  Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
+  Lemma dfrac_valid_discarded : ✓ DfracDiscarded.
   Proof. done. Qed.
 
   Lemma dfrac_valid_own_discarded q :
-- 
GitLab