Test.

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)"
+

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.