diff --git a/ci/simple-tests/omit_test.v b/ci/simple-tests/omit_test.v index f0382c5e3..53ccfbd3a 100644 --- a/ci/simple-tests/omit_test.v +++ b/ci/simple-tests/omit_test.v @@ -44,7 +44,7 @@ Qed. Section let_test. Let never_omit_let : 1 + 1 = 2. - Proof using. + Proof. (* automatic test marker 7 *) auto. Qed.