From e440e51b6e00c3f6cff715f6753ba7e3c641048e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Apr 2022 23:30:00 +0200
Subject: [PATCH] Tests.

---
 tests/proofmode.ref | 23 +++++++++++++++++++++++
 tests/proofmode.v   | 16 ++++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ce21d1c9d..58739cd69 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -396,6 +396,29 @@ No applicable tactic.
   "HQ" : Q
   --------------------------------------∗
   ▷ P ∗ Q
+"test_iRevert_pure"
+     : string
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P : PROP
+  ============================
+  "H" : <affine> ⌜φ⌝ -∗ P
+  --------------------------------------∗
+  <affine> ⌜φ⌝ -∗ P
+"test_iRevert_pure_affine"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P : PROP
+  ============================
+  "H" : ⌜φ⌝ -∗ P
+  --------------------------------------∗
+  ⌜φ⌝ -∗ P
 "elim_mod_accessor"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8ad3f6da4..e83bd50bf 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1146,6 +1146,22 @@ Proof.
   iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
 Qed.
 
+Check "test_iRevert_pure".
+Lemma test_iRevert_pure (φ : Prop) P :
+  φ → (<affine> ⌜ φ ⌝ -∗ P) -∗ P.
+Proof.
+  (* Check that iRevert creates a wand instead of an implication *)
+  iIntros (Hφ) "H". iRevert (Hφ). Show. done.
+Qed.
+
+Check "test_iRevert_pure_affine".
+Lemma test_iRevert_pure_affine `{!BiAffine PROP} (φ : Prop) P :
+  φ → (⌜ φ ⌝ -∗ P) -∗ P.
+Proof.
+  (* If the BI is affine, no affine modality should be added *)
+  iIntros (Hφ) "H". iRevert (Hφ). Show. done.
+Qed.
+
 End tests.
 
 Section parsing_tests.
-- 
GitLab