From d066da8381986aeba85f98f2bd395a5710a4a4e4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 17 Feb 2023 15:41:21 +0100
Subject: [PATCH] Alternative definition of `no_new_unsolved_evars` tactic by
 @jung.

---
 stdpp/tactics.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index 826f602e..eb30fabb 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -722,10 +722,9 @@ Lemma forall_and_distr (A : Type) (P Q : A → Prop) :
 Proof. firstorder. Qed.
 
 (** The tactic [no_new_unsolved_evars tac] executes [tac] and fails if it
-creates any new evars. This trick is by Jonathan Leivent, see:
-https://coq.inria.fr/bugs/show_bug.cgi?id=3872 *)
+creates any new evars. *)
 
-Ltac no_new_unsolved_evars tac := exact ltac:(tac).
+Ltac no_new_unsolved_evars tac := solve [unshelve tac].
 
 Tactic Notation "naive_solver" tactic(tac) :=
   unfold iff, not in *;
-- 
GitLab