diff --git a/CHANGES b/CHANGES index 3c5bcec8d..3c2e54ffb 100644 --- a/CHANGES +++ b/CHANGES @@ -5,7 +5,9 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG * Changes of Proof General 4.6 from Proof General 4.5 -N/A +** Coq changes + +*** support Coq 8.19 * Changes of Proof General 4.5 from Proof General 4.4 diff --git a/ci/compile-tests/010-coqdep-errors/runtest.el b/ci/compile-tests/010-coqdep-errors/runtest.el index 646ff2a5b..73800a1b7 100644 --- a/ci/compile-tests/010-coqdep-errors/runtest.el +++ b/ci/compile-tests/010-coqdep-errors/runtest.el @@ -34,7 +34,6 @@ ;;; Define the tests (ert-deftest cct-coqdep-fail-on-require () - :expected-result (if (coq--post-v818) :failed :passed) "coqdep error on missing library in a require command is detected." ;; (setq cct--debug-tests t) ;; (setq coq--debug-auto-compilation t) @@ -97,7 +96,6 @@ (ert-deftest cct-coqdep-fail-on-require-in-dependency () - :expected-result (if (coq--post-v818) :failed :passed) "coqdep error because of a missing library in a dependency is detected." (let (coqdep-errror-in-response missing-module-in-response diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index f5a9da8bf..b19f697fe 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -523,7 +523,7 @@ or not." :safe (lambda (v) (cl-every #'stringp v))) (defcustom coq-coqdep-error-regexp - (concat "^\\*\\*\\* Warning: in file .*, library .* is required " + (concat "^\\(\\*\\*\\* \\)?Warning: in file .*, library[ \n].* is required " "and has not been found") "Regexp to match errors in the output of coqdep. coqdep indicates errors not always via a non-zero exit status,