diff --git a/tests/tactics.v b/tests/tactics.v
index c547e91324c4184c99c69df24baada388fc1edb0..11d0a3c581c2d06f6a9225ee94e2bcb8aca6d745 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -54,3 +54,18 @@ Proof. intros ?. rename select nat into m. exists m. done. Qed.
 
 Goal ∀ (P : nat → Prop), P 3 → P 4 → P 4.
 Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed.
+
+(** [mk_evar] works on things that coerce to types. *)
+(** This is a feature when we have packed structures, for example Iris's [ofe]
+(fields other than the carrier omitted). *)
+Structure ofe := Ofe { ofe_car :> Type }.
+Goal ∀ A : ofe, True.
+intros A.
+let x := mk_evar A in idtac.
+Abort.
+
+(** More surprisingly, it also works for other coercions into a
+universe, like [Is_true : bool → Prop]. *)
+Goal True.
+let x := mk_evar true in idtac.
+Abort.