From 35705c3c46a2a634789eaadb302ee2327b8b6059 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 17 Jul 2021 13:34:15 +0200
Subject: [PATCH] alternative implementation of mk_evar that keeps naive_solver
 working

---
 tests/tactics.v    | 18 ++++--------------
 theories/tactics.v | 16 ++++++++++++++--
 2 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/tests/tactics.v b/tests/tactics.v
index 715e747d..34f00ed7 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -55,20 +55,10 @@ 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.
+(** Regression tests for [naive_solver]. *)
+Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
+  (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
+Proof. naive_solver. Qed.
 
 (** Make sure that [done] is not called recursively when solving [is_Some],
 which might leave an unresolved evar before performing ex falso. *)
diff --git a/theories/tactics.v b/theories/tactics.v
index d3910a89..ba96fded 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -222,8 +222,20 @@ current context.
 
 This is usually a more useful behavior than Coq's [evar], which is a
 side-effecting tactic (not returning anything) that introduces a local
-definition into the context that holds the evar. *)
-Ltac mk_evar T := open_constr:(_ : T).
+definition into the context that holds the evar.
+Note that the obvious alternative [open_constr (_:T)] has subtly different
+behavior, see std++ issue 115.
+
+Usually, Ltacs cannot return a value and have a side-effect, but we use the
+trickd escribed 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 e := fresh in
+  let _ := match goal with _ => evar (e:T) end in
+  let e' := eval unfold e in e in
+  let _ := match goal with _ => clear e end in
+  e'.
 
 (** The tactic [eunify x y] succeeds if [x] and [y] can be unified, and fails
 otherwise. If it succeeds, it will instantiate necessary evars in [x] and [y].
-- 
GitLab