From 8c34ee705043ab9b73cf55bb0ecdcb031785a5be Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 3 Jun 2023 09:11:41 +0000
Subject: [PATCH] Explicitly mention DfracDiscarded in match.

---
 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 b44fb1ef8..5e2e7b458 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