prettify after iMod

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 }}
+  

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.

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 :=