Skip to content
Snippets Groups Projects
Commit 1a2061bd authored by Ralf Jung's avatar Ralf Jung
Browse files

tests/tactics: do not depend on variable name

parent e97b9309
No related branches found
No related tags found
No related merge requests found
Pipeline #41052 passed
......@@ -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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment