diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index ca1adceeb947f216f35a5d31f8c957c1588e899d..322dc616c1818ad315f3618e191f06a9961b8dd1 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -4,6 +4,7 @@ From iris.base_logic Require Import bi derived.
 From iris.prelude Require Import options.
 
 (** Internalized properties of our CMRA constructions. *)
+Local Coercion uPred_holds : uPred >-> Funclass.
 
 Section upred.
 Context {M : ucmra}.
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 672eaa7167f20fa9b90f687458c2345e3d38efea..c230062506c7a93233c622f4c2bbb7e41c23c889 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -240,7 +240,7 @@ End restate.
 
 
 (** New unseal tactic that also unfolds the BI layer.
-    This is used by [base_logic.bupd_alt].
+    This is used by [base_logic.algebra] and [base_logic.bupd_alt].
     TODO: Can we get rid of this? *)
 Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
   unfold bi_emp; simpl;
diff --git a/iris/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
index 898511d53a80e2990da7a3c66ae6ff33ac515fe4..5c6868233d08f3a66277337671d2979b466c98f2 100644
--- a/iris/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
@@ -25,6 +25,8 @@ We show that:
 
 The first two points are shown for any BI with a plain modality. *)
 
+Local Coercion uPred_holds : uPred >-> Funclass.
+
 Section bupd_alt.
   Context `{BiPlainly PROP}.
   Implicit Types P Q R : PROP.
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 237149e76c3400bc6a30022ab72c7ece43c3e721..0a0d4d8bea8a1a7477a86ecd653efacca5fdec2f 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -105,11 +105,15 @@ This completes the proof.
 *)
 
 Record uPred (M : ucmra) : Type := UPred {
-  uPred_holds :> nat → M → Prop;
+  uPred_holds : nat → M → Prop;
 
   uPred_mono n1 n2 x1 x2 :
     uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → uPred_holds n2 x2
 }.
+(** When working in the model, it is convenient to be able to treat [uPred] as
+[nat → M → Prop].  But we only want to locally break the [uPred] abstraction
+this way. *)
+Local Coercion uPred_holds : uPred >-> Funclass.
 Bind Scope bi_scope with uPred.
 Global Arguments uPred_holds {_} _%I _ _ : simpl never.
 Add Printing Constructor uPred.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 4725abbccde6d7ff943b939e842a70985895ca38..94778022e8d41c14733a8af9dd8c84752a947018 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -6,9 +6,10 @@ From iris.prelude Require Import options.
 define the usual connectives of higher-order logic, and prove that these satisfy
 the usual laws of higher-order logic. *)
 Record siProp := SiProp {
-  siProp_holds :> nat → Prop;
+  siProp_holds : nat → Prop;
   siProp_closed n1 n2 : siProp_holds n1 → n2 ≤ n1 → siProp_holds n2
 }.
+Local Coercion siProp_holds : siProp >-> Funclass.
 Global Arguments siProp_holds : simpl never.
 Add Printing Constructor siProp.