[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 0d5ae06575: simple-tests/omit_test: fix Coq
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general 0d5ae06575: simple-tests/omit_test: fix Coq sources for 8.19 |
Date: |
Mon, 22 Jan 2024 04:00:51 -0500 (EST) |
branch: elpa/proof-general
commit 0d5ae06575cea0bbc66904323f1c620779514afa
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>
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.
---
ci/simple-tests/omit_test.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/ci/simple-tests/omit_test.v b/ci/simple-tests/omit_test.v
index f0382c5e35..53ccfbd3a0 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.
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [nongnu] elpa/proof-general 0d5ae06575: simple-tests/omit_test: fix Coq sources for 8.19,
ELPA Syncer <=