diff --git a/iris_plog.v b/iris_plog.v
index 99236e0c21850cd8b01b13d94a2e35a2149da80d..2195dbe6ef8e0f330dde8b5b10a5d0d12b870abc 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -102,11 +102,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     Qed.
 
     (* When is a resource okay with a state? *)
-    Definition res_sat (r: res) σ: Prop := ↓r /\
-      match fst r with
-        | ex_own s => s = σ
-        | _ => True (* We don't care. Note that validity is ensured by the first conjunct. *)
-      end.
+    Definition res_sat (r: res) σ: Prop := ↓r /\ fst r == ex_own state σ.
 
     Global Instance res_sat_dist : Proper (equiv ==> equiv ==> iff) res_sat.
     Proof.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 1b88f573cfb7ec1eee173c3923f9b4a21357a37b..458211d93853e1d24f8a67d20e4736185519fe88 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -1,4 +1,4 @@
-(** Resource algebras: Commutative monoids with a decidable validity predicate. *)
+(** Resource algebras: Commutative monoids with a validity predicate. *)
 
 Require Import Bool.
 Require Import Predom.