diff --git a/CHANGELOG.md b/CHANGELOG.md
index 22fb3c621b1b3536f9cbc390a87e3e65cc852a44..9dfd0a3f29a591eade0677aea06506e017e02adb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,8 @@ Coq 8.13 is no longer supported.
   `_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish
   proofs. (by Ike Mulder)
 * Rename `singleton_mono` to `singleton_included_mono`.
+* Use `Strategy expand` for CMRA/UCMRA coercions and most projections to improve
+  performance of type-checking some large CMRA/OFE types. (by Ike Mulder)
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 4b14550a1fcbcb6dd002a0827702ceba0e9da80e..f14a8ebe4d10bb238a0694106892cf60b4619b6a 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -106,6 +106,19 @@ Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_in
 Coercion cmra_ofeO (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
 Canonical Structure cmra_ofeO.
 
+(** As explained more thoroughly in iris#539, Coq can run into trouble when
+  [cmra] combinators (such as [optionUR]) are stacked and combined with
+  coercions like [cmra_ofeO]. To partially address this, we give Coq's
+  type-checker some directions for unfolding, with the Strategy command.
+
+  For these structures, we instruct Coq to eagerly _expand_ all projections,
+  except for the coercion to type (in this case, [cmra_car]), since that causes
+  problem with canonical structure inference. Additionally, we make Coq 
+  eagerly expand the coercions that go from one structure to another, like
+  [cmra_ofeO] in this case. *)
+Global Strategy expand [cmra_ofeO cmra_equiv cmra_dist cmra_pcore cmra_op
+                        cmra_valid cmra_validN cmra_ofe_mixin cmra_mixin].
+
 Definition cmra_mixin_of' A {Ac : cmra} (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac.
 Notation cmra_mixin_of A :=
   ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
@@ -232,6 +245,15 @@ Coercion ucmra_cmraR (A : ucmra) : cmra :=
   Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
 Canonical Structure ucmra_cmraR.
 
+(** As for CMRAs above, we instruct Coq to eagerly _expand_ all projections,
+  except for the coercion to type (in this case, [ucmra_car]), since that causes
+  problem with canonical structure inference.  Additionally, we make Coq 
+  eagerly expand the coercions that go from one structure to another, like
+  [ucmra_cmraR] and [ucmra_ofeO] in this case. *)
+Global Strategy expand [ucmra_cmraR ucmra_ofeO ucmra_equiv ucmra_dist ucmra_pcore
+                        ucmra_op ucmra_valid ucmra_validN ucmra_unit
+                        ucmra_ofe_mixin ucmra_cmra_mixin].
+
 (** Lifting properties from the mixin *)
 Section ucmra_mixin.
   Context {A : ucmra}.