From 1a2061bda176fded648b87ced1b3ada3809952e8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Jan 2021 18:46:35 +0100
Subject: [PATCH] tests/tactics: do not depend on variable name

---
 tests/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/tactics.v b/tests/tactics.v
index 29e27969..c547e913 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -53,4 +53,4 @@ Goal ∀ (n : nat), ∃ m : nat, True.
 Proof. intros ?. rename select nat into m. exists m. done. Qed.
 
 Goal ∀ (P : nat → Prop), P 3 → P 4 → P 4.
-Proof. intros. rename select (P _) into HP4. apply HP4. Qed.
+Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed.
-- 
GitLab