From 90debd5bcc09b39b43282544e8627deb762cd6b7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Jun 2023 00:44:20 +0200
Subject: [PATCH] Remove `frac_validI`.

---
 iris/base_logic/algebra.v                   | 3 ---
 iris/base_logic/lib/cancelable_invariants.v | 2 +-
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 34fba7aef..e3272890b 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -23,9 +23,6 @@ Section upred.
     ✓ g ⊣⊢ ∀ i, ✓ g i.
   Proof. by uPred.unseal. Qed.
 
-  Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
-  Proof. rewrite uPred.discrete_valid frac_valid //. Qed.
-
   Section gmap_ofe.
     Context `{Countable K} {A : ofe}.
     Implicit Types m : gmap K A.
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 913ddb925..e9df6b26d 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -47,7 +47,7 @@ Section proofs.
   Proof. split; [done|]. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
-  Proof. rewrite -frac_validI. apply (own_valid_2 γ q1 q2). Qed.
+  Proof. rewrite -frac_valid -uPred.discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
 
   Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
   Proof.
-- 
GitLab