From 928684f973cb2bf3e879243cd6a4939df8631e28 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 28 Jun 2021 20:37:11 +0200
Subject: [PATCH] add test for mk_evar and things that coerce to types

---
 tests/tactics.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/tests/tactics.v b/tests/tactics.v
index c547e913..11d0a3c5 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.
-- 
GitLab