diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index dd0a97deb14a04079ce99287cc89829111356a9e..61197930c830bbb5941f78dea7fd448dd8ede82d 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -1,3 +1,5 @@
+"demo_0"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -19,6 +21,8 @@
   --------------------------------------â–¡
   Q ∨ P
   
+"test_iDestruct_and_emp"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -59,6 +63,8 @@ In nested Ltac calls to "iSpecialize (open_constr)",
 "iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
 failed.
 Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
+"test_iNext_plus_3"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -68,6 +74,8 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   â–·^(S n + S m) emp
   
+"test_iFrame_later_1"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -76,6 +84,8 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   â–· emp
   
+"test_iFrame_later_2"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -89,6 +99,8 @@ In nested Ltac calls to "iFrame (constr)",
 "<iris.proofmode.ltac_tactics.iFrame_go>" and
 "<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
 Tactic failure: iFrame: cannot frame Q.
+"test_and_sep_affine_bi"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -100,6 +112,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   â–¡ P
   
+"test_big_sepL_simpl"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -126,6 +140,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P
   
+"test_big_sepL2_simpl"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -153,6 +169,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
   
+"test_big_sepL2_iDestruct"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -165,6 +183,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   <absorb> Φ x1 x2
   
+"test_reducing_after_iDestruct"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -173,6 +193,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   True
   
+"test_reducing_after_iApply"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -181,6 +203,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------â–¡
   â–¡ emp
   
+"test_reducing_after_iApply_late_evar"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -189,6 +213,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------â–¡
   â–¡ emp
   
+"test_wandM"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -197,7 +223,7 @@ Tactic failure: iFrame: cannot frame Q.
   ============================
   "HPQ" : mP -∗? Q
   "HQR" : Q -∗ R
-  "HP" : pm_default emp mP
+  "HP" : default emp mP
   --------------------------------------∗
   R
   
@@ -207,10 +233,28 @@ Tactic failure: iFrame: cannot frame Q.
   mP : option PROP
   Q, R : PROP
   ============================
-  "HP" : pm_default emp mP
+  "HP" : default emp mP
+  --------------------------------------∗
+  default emp mP
+  
+"elim_mod_accessor"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  X : Type
+  E1, E2 : coPset.coPset
+  α : X → PROP
+  β : X → PROP
+  γ : X → option PROP
+  ============================
+  "Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
   --------------------------------------∗
-  pm_default emp mP
+  |={E2,E1}=> True
   
+"print_long_line_1"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -233,6 +277,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   True
   
+"print_long_line_2"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -255,6 +301,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   True
   
+"long_impl"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -265,6 +313,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP
   → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_impl_nested"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -276,6 +326,8 @@ Tactic failure: iFrame: cannot frame Q.
   → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
     → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_wand"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -286,6 +338,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP
   -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_wand_nested"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -297,6 +351,8 @@ Tactic failure: iFrame: cannot frame Q.
   -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
      -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_fupd"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -308,6 +364,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP
   ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_fupd_nested"
+     : string
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7cef4f3e7a5b0dbdb7a06302f8f0df864496b461..462866768bc8e1251b85212b4bd8dccdd2707953 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -6,6 +6,7 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
+Check "demo_0".
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
   iIntros "H #H2". Show. iDestruct "H" as "###H".
@@ -52,6 +53,7 @@ Proof.
   auto.
 Qed.
 
+Check "test_iDestruct_and_emp".
 Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
   P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).
 Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
@@ -365,6 +367,7 @@ Lemma test_iNext_plus_1 P n1 n2 : ▷ ▷^n1 ▷^n2 P -∗ ▷^n1 ▷^n2 ▷ P.
 Proof. iIntros "H". iNext. iNext. by iNext. Qed.
 Lemma test_iNext_plus_2 P n m : ▷^n ▷^m P -∗ ▷^(n+m) P.
 Proof. iIntros "H". iNext. done. Qed.
+Check "test_iNext_plus_3".
 Lemma test_iNext_plus_3 P Q n m k :
   ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q).
 Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
@@ -408,9 +411,11 @@ Lemma test_iPureIntro_absorbing (φ : Prop) :
   φ → sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
 Proof. intros ?. iPureIntro. done. Qed.
 
+Check "test_iFrame_later_1".
 Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". Show. auto. Qed.
 
+Check "test_iFrame_later_2".
 Lemma test_iFrame_later_2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (▷ P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". Show. auto. Qed.
 
@@ -480,11 +485,13 @@ Proof.
   - iDestruct "H" as "[_ [_ #$]]".
 Qed.
 
+Check "test_and_sep_affine_bi".
 Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   iIntros "[??]". iSplit; last done. Show. done.
 Qed.
 
+Check "test_big_sepL_simpl".
 Lemma test_big_sepL_simpl x (l : list nat) P :
    P -∗
   ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
@@ -492,6 +499,7 @@ Lemma test_big_sepL_simpl x (l : list nat) P :
   P.
 Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
 
+Check "test_big_sepL2_simpl".
 Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
   P -∗
   ([∗ list] k↦y1;y2 ∈ []; l2, <affine> ⌜ y1 = y2 ⌝) -∗
@@ -499,6 +507,7 @@ Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
   P ∨ ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, True).
 Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
 
+Check "test_big_sepL2_iDestruct".
 Lemma test_big_sepL2_iDestruct (Φ : nat → nat → PROP) x1 x2 (l1 l2 : list nat) :
   ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, Φ y1 y2) -∗
   <absorb> Φ x1 x2.
@@ -512,6 +521,7 @@ Proof. iIntros "$ ?". iFrame. Qed.
 Lemma test_lemma_1 (b : bool) :
   emp ⊢@{PROP} □?b True.
 Proof. destruct b; simpl; eauto. Qed.
+Check "test_reducing_after_iDestruct".
 Lemma test_reducing_after_iDestruct : emp ⊢@{PROP} True.
 Proof.
   iIntros "H". iDestruct (test_lemma_1 true with "H") as "H". Show. done.
@@ -520,6 +530,7 @@ Qed.
 Lemma test_lemma_2 (b : bool) :
   □?b emp ⊢@{PROP} emp.
 Proof. destruct b; simpl; eauto. Qed.
+Check "test_reducing_after_iApply".
 Lemma test_reducing_after_iApply : emp ⊢@{PROP} emp.
 Proof.
   iIntros "#H". iApply (test_lemma_2 true). Show. auto.
@@ -528,6 +539,7 @@ Qed.
 Lemma test_lemma_3 (b : bool) :
   □?b emp ⊢@{PROP} ⌜b = b⌝.
 Proof. destruct b; simpl; eauto. Qed.
+Check "test_reducing_after_iApply_late_evar".
 Lemma test_reducing_after_iApply_late_evar : emp ⊢@{PROP} ⌜true = true⌝.
 Proof.
   iIntros "#H". iApply (test_lemma_3). Show. auto.
@@ -535,6 +547,7 @@ Qed.
 
 Section wandM.
   Import proofmode.base.
+  Check "test_wandM".
   Lemma test_wandM mP Q R :
     (mP -∗? Q) -∗ (Q -∗ R) -∗ (mP -∗? R).
   Proof.
@@ -544,6 +557,27 @@ Section wandM.
   Qed.
 End wandM.
 
+Definition modal_if_def b (P : PROP) :=
+  (â–¡?b P)%I.
+Lemma modal_if_lemma1 b P :
+  False -∗ □?b P.
+Proof. iIntros "?". by iExFalso. Qed.
+Lemma test_iApply_prettification1 (P : PROP) :
+  False -∗ modal_if_def true P.
+Proof.
+  (* Make sure the goal is not prettified before [iApply] unifies. *)
+  iIntros "?". rewrite /modal_if_def. iApply modal_if_lemma1. iAssumption.
+Qed.
+Lemma modal_if_lemma2 P :
+  False -∗ □?false P.
+Proof. iIntros "?". by iExFalso. Qed.
+Lemma test_iApply_prettification2 (P  : PROP) :
+  False -∗ ∃ b, □?b P.
+Proof.
+  (* Make sure the conclusion of the lemma is not prettified too early. *)
+  iIntros "?". iExists _. iApply modal_if_lemma2. done.
+Qed.
+
 End tests.
 
 (** Test specifically if certain things print correctly. *)
@@ -551,9 +585,15 @@ Section printing_tests.
 Context {PROP : sbi} `{!BiFUpd PROP}.
 Implicit Types P Q R : PROP.
 
+Check "elim_mod_accessor".
+Lemma elim_mod_accessor {X : Type} E1 E2 α (β : X → PROP) γ :
+  accessor (fupd E1 E2) (fupd E2 E1) α β γ -∗ |={E1}=> True.
+Proof. iIntros ">Hacc". Show. Abort.
+
 (* Test line breaking of long assumptions. *)
 Section linebreaks.
-Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
+Check "print_long_line_1".
+Lemma print_long_line_1 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
   P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
   P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
   -∗ True.
@@ -565,38 +605,45 @@ Abort.
    the proofmode notation breaks the output. *)
 Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P ∧ Q)%I
   (format "'TESTNOTATION'  '{{'  P  '|'  '/' Q  '}' '}'") : bi_scope.
-Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
+Check "print_long_line_2".
+Lemma print_long_line_2 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
   TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
   -∗ True.
 Proof.
   iIntros "HP". Show. Undo. iIntros "?". Show.
 Abort.
 
+Check "long_impl".
 Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_impl_nested".
 Lemma long_impl_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_wand".
 Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_wand_nested".
 Lemma long_wand_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_fupd".
 Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_fupd_nested".
 Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   PPPPPPPPPPPPPPPPP ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 2ebd9d88381ea6cc641afbf0599f75fba975848d..d1adf1666b32c49aa063712ca6c7534589c77276 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -385,7 +385,7 @@ Proof.
 Qed.
 
 Global Instance into_wand_wandM p q mP' P Q :
-  FromAssumption q P (pm_default emp%I mP') → IntoWand p q (mP' -∗? Q) P Q.
+  FromAssumption q P (default emp%I mP') → IntoWand p q (mP' -∗? Q) P Q.
 Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.
 
 Global Instance into_wand_and_l p q R1 R2 P' Q' :
@@ -510,7 +510,7 @@ Qed.
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
 Proof. by rewrite /FromWand. Qed.
 Global Instance from_wand_wandM mP1 P2 :
-  FromWand (mP1 -∗? P2) (pm_default emp mP1)%I P2.
+  FromWand (mP1 -∗? P2) (default emp mP1)%I P2.
 Proof. by rewrite /FromWand wandM_sound. Qed.
 Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
@@ -1079,6 +1079,9 @@ Proof.
   - iApply (Hacc with "Hinv Hin"). done.
 Qed.
 
+(* This uses [pm_default] because, after inference, all accessors will have
+[None] or [Some _] there, so we want to reduce the combinator before showing the
+goal to the user. *)
 Global Instance elim_inv_acc_with_close {X : Type}
        φ1 φ2 Pinv Pin
        M1 M2 α β mγ Q Q' :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 43b2697330831d60eca6e7e3960bc316eb9d9e00..b490382401fb15c37c1999a336b993ba1b2193da 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -526,7 +526,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
     instances to recognize the [emp] case and make it look nicer. *)
 Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
            (α β : X → PROP) (mγ : X → option PROP) : PROP :=
-  M1 (∃ x, α x ∗ (β x -∗ M2 (pm_default emp (mγ x))))%I.
+  M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
 
 (* Typeclass for assertions around which accessors can be elliminated.
    Inputs: [Q], [E1], [E2], [α], [β], [γ]
@@ -582,7 +582,7 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
 Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
       (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
       (Q : PROP) (Q' : X → PROP) :=
-  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (pm_default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
+  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
 Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
 Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
 Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 724c9dcf4e048cc26e9cdf34b5e694476448472e..b54edbd4d91808d4974bb42693c1f3042320d6cb 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1108,7 +1108,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
     lazymatch pats with
     | [] =>
       lazymatch found with
-      | true => idtac
+      | true => pm_prettify (* post-tactic prettification *)
       | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
       end
     | ISimpl :: ?pats => simpl; find_pat found pats
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index cda25a14c4a11d66ec28370877ba9f667e76a117..d13067c9b8c6cbb81743d1d7f0158cdef7c093c9 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -1,7 +1,10 @@
 From iris.bi Require Import bi telescopes.
 From iris.proofmode Require Import base environments.
 
-Declare Reduction pm_cbv := cbv [
+(** Called by all tactics to perform computation to lookup items in the
+    context.  We avoid reducing anything user-visible here to make sure we
+    do not reduce e.g. before unification happens in [iApply].*)
+Declare Reduction pm_eval := cbv [
   (* base *)
   base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
   (* environments *)
@@ -11,13 +14,18 @@ Declare Reduction pm_cbv := cbv [
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_persistent envs_incr_counter
   envs_split_go envs_split prop_of_env
-].
-(* Some things should only be unfolded according to cbn rules, when
-   certain arguments are constructors. This is because they can appear in
-   the user side of proofs as well. *)
-Declare Reduction pm_cbn := cbn [
   (* PM option combinators *)
   pm_option_bind pm_from_option pm_option_fun
+].
+Ltac pm_eval t :=
+  eval pm_eval in t.
+Ltac pm_reduce :=
+  match goal with |- ?u => let v := pm_eval u in change v end.
+Ltac pm_reflexivity := pm_reduce; exact eq_refl.
+
+(** Called by many tactics for redexes that are created by instantiation.
+    This cannot create any envs redexes so we just do the cbn part. *)
+Declare Reduction pm_prettify := cbn [
   (* telescope combinators *)
   tele_fold tele_bind tele_app
   (* BI connectives *)
@@ -25,15 +33,5 @@ Declare Reduction pm_cbn := cbn [
   bi_wandM sbi_laterN
   bi_tforall bi_texist
 ].
-Ltac pm_eval t :=
-  let u := eval pm_cbv in t in
-  let v := eval pm_cbn in u in
-  v.
-Ltac pm_reduce :=
-  match goal with |- ?u => let v := pm_eval u in change v end.
-Ltac pm_reflexivity := pm_reduce; exact eq_refl.
-
-(** Called e.g. by iApply for redexes that are created by instantiation.
-    This cannot create any envs redexes so we just to the cbn part. *)
 Ltac pm_prettify :=
-  match goal with |- ?u => let v := eval pm_cbn in u in change v end.
+  match goal with |- ?u => let v := eval pm_prettify in u in change v end.