diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index af9cbbdea8690a0590b6a401fd7db14bcbe98fdc..21fe9145e78befdbc682283e7dfe74d25e93d3f7 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -3,6 +3,11 @@ From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
 From iris.prelude Require Import options.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 656ce78835dd3c0b09a7f41e3cf79eb77c668864..a905be1894e3ac12da98166bf7b8268b401ffb55 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -1,7 +1,11 @@
 From iris.algebra Require Export ofe.
 From iris.bi Require Export notation.
 From iris.prelude Require Import options.
-Set Primitive Projections.
+
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
 
 Section bi_mixin.
   Context {PROP : Type} `{!Dist PROP, !Equiv PROP}.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 4ad7f1dcda44006423b2451c1f8b00f527850e64..1353e7ddf9bfdd616307a388aed34e9247e69d65 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -2,6 +2,11 @@ From iris.bi Require Import derived_laws_later big_op.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (** This file defines a type class for BIs with a notion of internal equality.
 Internal equality is not part of the [bi] canonical structure as [internal_eq]
 can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 4edbb20de06ccab7b9eb1ec436a83dd0cf42a116..7404ef443eaeab350ec720c7ab827a44a5f95fdf 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -3,6 +3,11 @@ From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 74d22bd3242e427105bc36ce9e1fd5aea5cef370..359a8dc9eb29759bf65119e1b8c2a65c3e6e775c 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -3,6 +3,11 @@ From iris.bi Require Import interface derived_laws_later big_op plainly.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index f85b167b4a75467c954fcb064dcc818cd93f1355..0ffa2e841437fb2951e4a2cd6919b4bd2369fc8f 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -174,7 +174,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   @bi_emp_valid (uPredI (iResUR Σ))
     (@fupd (bi_car (uPredI (iResUR Σ)))
-       (@bi_fupd_fupd (uPredI (iResUR Σ))
+       (@bi_fupd_fupd _
           (@uPred_bi_fupd HasLc Σ
              (@iris_invGS HasLc heap_lang Σ (@heapGS_irisGS HasLc Σ heapGS0))))
        (@top coPset coPset_top) (@top coPset coPset_top)