diff --git a/tests/bi.ref b/tests/bi.ref
index 3501bc76ecfd2a8f1b503ae9b870dda364b97a14..27b5cb7da314682827854e7c3ab45e03ea45a9bb 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 299a8bd3da335b979195624b4babcb3919896555..3e38ccce0141b0fe4696c2d13840e7c2170ea205 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.