From 95a9135a222584f5194af718a5593cec2f0fd7d7 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Tue, 6 Jun 2023 15:16:46 +0200
Subject: [PATCH] Whoops, 8c34ee70 got eaten before

---
 iris/base_logic/algebra.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 7d3e7e422..4a830663c 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -30,7 +30,7 @@ Section upred.
     ✓ dq ⊣⊢ match dq with
             | DfracOwn q => ⌜q ≤ 1⌝%Qp
             | DfracBoth q => ⌜q < 1⌝%Qp
-            | _ => True
+            | DfracDiscarded => True
             end.
   Proof. destruct dq; by rewrite uPred.discrete_valid. Qed.
 
-- 
GitLab