diff --git a/tests/atomic.ref b/tests/atomic.ref
index 864ff13700f6a594c1fc9049be4ba2fd06b537a5..238708315a1656731ecc3a853489338db7c99e9d 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -338,3 +338,34 @@
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
+"Prettification"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  ============================
+  --------------------------------------∗
+  ∀ Φ : language.val heap_lang → iProp Σ, AU << ∀ 
+                                             x : val, 
+                                             P x >> @ ⊤, ∅
+                                             << ∃ y : val, P y, COMM Φ #() >>
+                                          -∗ WP ! #0 {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  "AU" : ∃ x : val, P x
+                    ∗ (P x
+                       ={∅,⊤}=∗ AU << ∀ x0 : val, 
+                                   P x0 >> @ ⊤, ∅
+                                   << ∃ y : val, P y, COMM Φ #() >>)
+                      ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
+  --------------------------------------∗
+  WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
+  
diff --git a/tests/atomic.v b/tests/atomic.v
index 87efeb553794d71993524d191bd6af104b71d721..9f2b7dd34229a244f597cbfa719ea7afbe02445a 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -88,4 +88,13 @@ Section printing.
     Show. iIntros (Q Φ) "? AU". Show.
   Abort.
 
+  Check "Prettification".
+
+  Lemma iMod_prettify (P : val → iProp Σ) :
+    <<< ∀ x, P x >>> !#0 @ ⊤ <<< ∃ y, P y, RET #() >>>.
+  Proof.
+    iApply wp_atomic_intro. Show.
+    iIntros (Φ) "AU". iMod "AU". Show.
+  Abort.
+
 End printing.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 34763324e3ddeaa701f90158bfebe268f19d9831..c33ca55e0423f073497539a880af12b71c870697 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1214,7 +1214,7 @@ Tactic Notation "iModCore" constr(H) :=
      fail "iMod: cannot eliminate modality" P "in" Q
     |iSolveSideCondition
     |pm_reflexivity
-    |(* subgoal *)].
+    |pm_prettify(* subgoal *)].
 
 (** * Basic destruct tactic *)
 Local Ltac iDestructHypGo Hz pat :=