diff --git a/tests/bi.v b/tests/bi.v index 92f797609a9d6fb3d00f982206b91dd3ba0f6d9a..1dc3b77c641a09563f99723825672070f96640ad 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.