From 67a490f6100822feb26672a5f536bc497461d1a3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Jul 2023 12:25:05 +0200
Subject: [PATCH] Add test.

---
 tests/proofmode.ref |  8 ++++++++
 tests/proofmode.v   | 10 ++++++++++
 2 files changed, 18 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 5d08d96a1..480eb6486 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -628,6 +628,14 @@ No applicable tactic.
   "H" : <affine> ⌜φ⌝ -∗ P
   --------------------------------------∗
   <affine> ⌜φ⌝ -∗ P
+"test_iRevert_order_and_names"
+     : string
+1 goal
+  
+  PROP : bi
+  ============================
+  --------------------------------------∗
+  ∀ P1 P2, P1 -∗ P2 -∗ P1 ∗ P2
 "test_iRevert_pure_affine"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7ebd11da3..477fddf38 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1428,6 +1428,16 @@ Proof.
   iIntros (Hφ) "H". iRevert (Hφ). Show. done.
 Qed.
 
+Check "test_iRevert_order_and_names".
+Lemma test_iRevert_order_and_names P1 P2 : P1 -∗ P2 -∗ P1 ∗ P2.
+Proof.
+  iIntros "H1 H2". iRevert (P1 P2) "H1 H2".
+  (* Check that the reverts are performed in the right order (i.e., reverse),
+  and that the names [P1] and [P2] are used in the goal. *)
+  Show.
+  auto with iFrame.
+Qed.
+
 Check "test_iRevert_pure_affine".
 Lemma test_iRevert_pure_affine `{!BiAffine PROP} (φ : Prop) P :
   φ → (⌜ φ ⌝ -∗ P) -∗ P.
-- 
GitLab