From b600a5bb738a39e56d4eb29073e5a5450aeed03a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 13 May 2021 15:08:29 +0200
Subject: [PATCH] test bi Lemma scopes

---
 tests/bi.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/tests/bi.v b/tests/bi.v
index 92f797609..1dc3b77c6 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -7,3 +7,10 @@ Proof. apply _. Qed.
 Lemma test_impl_persistent_2 `{!BiPlainly PROP} :
   Persistent (PROP:=PROP) (True → True → True).
 Proof. apply _. Qed.
+
+(* Test that the right scopes are used. *)
+Lemma test_bi_scope {PROP : bi} : True.
+Proof.
+  (* [<affine> True] is implicitly in %I scope. *)
+  pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
+Abort.
-- 
GitLab