diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index 826f602eeba9014175bcd82cb71f3e559cf9c4cd..eb30fabb5d2a847ffa2c8b1d1c2e920d32d3c8a1 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 *;