simple-tests/omit_test: fix Coq sources for 8.19

8.19 does not tolerate Proof using after let. Until now this problem was hidden by the two expected fails.
ProofGeneral · Jan 22, 2024 · 0d5ae06 · 0d5ae06
1 parent 311a6b7
commit 0d5ae06
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.