diff --git a/tests/tactics.v b/tests/tactics.v
index 29e27969dc595e2b2f8e32eafb1439e8becf52b3..c547e91324c4184c99c69df24baada388fc1edb0 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.