diff --git a/src/dune_rules/coq/coq_stanza.ml b/src/dune_rules/coq/coq_stanza.ml index 4e3f946aac1..47180a2b2de 100644 --- a/src/dune_rules/coq/coq_stanza.ml +++ b/src/dune_rules/coq/coq_stanza.ml @@ -10,6 +10,7 @@ let coq_syntax = ; ((0, 5), `Since (3, 4)) ; ((0, 6), `Since (3, 5)) ; ((0, 7), `Since (3, 7)) + ; ((0, 8), `Since (3, 8)) ] module Coqpp = struct diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t index e71a416e3f4..fb299b6d48e 100644 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t +++ b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-root.t/run.t @@ -14,5 +14,5 @@ This test is currently broken due to the workspace resolution being faulty #5899 1 | (coq.theory 2 | (name foo)) Error: 'coq.theory' is available only when coq is enabled in the dune-project - file. You must enable it using (using coq 0.7) in your dune-project file. + file. You must enable it using (using coq 0.8) in your dune-project file. [1] diff --git a/test/blackbox-tests/test-cases/coq/github3624.t b/test/blackbox-tests/test-cases/coq/github3624.t index 56919667f68..f5145f2a235 100644 --- a/test/blackbox-tests/test-cases/coq/github3624.t +++ b/test/blackbox-tests/test-cases/coq/github3624.t @@ -1,7 +1,7 @@ -This used to be a reproduction case for #3624, where dune created a -dune-project with an incorrect using line. Since we dropped support -for automatically creating the dune-project file, this is now testing -that the error message is good when the coq extension is not enabled. +This used to be a reproduction case for #3624, where dune created a dune-project +with an incorrect using line. Since we dropped support for automatically +creating the dune-project file, this is now testing that the error message is +good when the coq extension is not enabled. $ cat >dune < (coq.theory @@ -16,5 +16,5 @@ that the error message is good when the coq extension is not enabled. 1 | (coq.theory 2 | (name foo)) Error: 'coq.theory' is available only when coq is enabled in the dune-project - file. You must enable it using (using coq 0.7) in your dune-project file. + file. You must enable it using (using coq 0.8) in your dune-project file. [1]