From d21b227fe7b49a92258670fed9132cacf12f6ece Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 10:38:16 +0200
Subject: [PATCH] Test.
---
tests/bi.ref | 16 ++++++++++++++++
tests/bi.v | 10 ++++++++++
2 files changed, 26 insertions(+)
diff --git a/tests/bi.ref b/tests/bi.ref
index 3501bc76e..27b5cb7da 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -4,3 +4,19 @@ PROP : bi
m : gmap nat nat
The term "m" has type "gmap nat nat" while it is expected to have type
"gmap nat Z" (cannot unify "nat" and "Z").
+The command has indeed failed with message:
+Unable to satisfy the following constraints:
+In environment:
+PROP : bi
+P : PROP
+
+?p : "Persistent (|==> P)"
+
+The command has indeed failed with message:
+Unable to satisfy the following constraints:
+In environment:
+PROP : bi
+P : PROP
+
+?p : "Persistent (â– P)"
+
diff --git a/tests/bi.v b/tests/bi.v
index 299a8bd3d..3e38ccce0 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -60,3 +60,13 @@ Section big_sepM_implicit_type.
Definition big_sepM_implicit_type {PROP : bi} (m : gmap nat nat) : PROP :=
[∗ map] x ∈ m, ⌜ 10%Z = x âŒ.
End big_sepM_implicit_type.
+
+(** This tests that [bupd] is [Typeclasses Opaque]. If [bupd] were transparent,
+Coq would unify [bupd_instance] with [persistently]. *)
+Goal ∀ {PROP : bi} (P : PROP),
+ ∃ bupd_instance, Persistent (@bupd PROP bupd_instance P).
+Proof. intros. eexists _. Fail apply _. Abort.
+(* Similarly for [plainly]. *)
+Goal ∀ {PROP : bi} (P : PROP),
+ ∃ plainly_instance, Persistent (@plainly PROP plainly_instance P).
+Proof. intros. eexists _. Fail apply _. Abort.
--
GitLab