emacs-elpa-diffs
[Top][All Lists]
Advanced

[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.



reply via email to

[Prev in Thread] Current Thread [Next in Thread]