From 0c51eb83425bb4feb4ba4d54ada4286d26c4281b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 19 Jan 2019 11:55:48 +0000
Subject: [PATCH] prettify after iMod

---
 tests/atomic.ref                  | 31 +++++++++++++++++++++++++++++++
 tests/atomic.v                    |  9 +++++++++
 theories/proofmode/ltac_tactics.v |  2 +-
 3 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/tests/atomic.ref b/tests/atomic.ref
index 864ff1370..238708315 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 87efeb553..9f2b7dd34 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 34763324e..c33ca55e0 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 :=
-- 
GitLab