From 7a1421d1c4058ef6203b707ef21c4d1cd7a201a4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 19 Jul 2021 12:26:50 +0200
Subject: [PATCH] preserve mk_evar support for type coercions (by Robbert)

---
 tests/tactics.v    | 14 ++++++++++++++
 theories/tactics.v |  1 +
 2 files changed, 15 insertions(+)

diff --git a/tests/tactics.v b/tests/tactics.v
index 34f00ed7..b91a4733 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -60,6 +60,20 @@ Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
   (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
 Proof. naive_solver. 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.
+
 (** Make sure that [done] is not called recursively when solving [is_Some],
 which might leave an unresolved evar before performing ex falso. *)
 Goal False → is_Some (@None nat).
diff --git a/theories/tactics.v b/theories/tactics.v
index 6ed5877f..6ec949e0 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -231,6 +231,7 @@ trick described at
 <https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884>
 to work around that: wrap the side-effect in a [match goal]. *)
 Ltac mk_evar T :=
+  let T := constr:(T : Type) in
   let e := fresh in
   let _ := match goal with _ => evar (e:T) end in
   let e' := eval unfold e in e in
-- 
GitLab