add Coq compile test for a delayed require

2 files changed, 1 insertions, 11 deletions

diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 29c1ddab..e8512068 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -33,16 +33,6 @@
 ;; Note that all argument computations inherit `coq-autodetected-version': when
 ;; changing compilers, all compilation jobs must be terminated.  This is
 ;; consistent with the fact that the _CoqProject file is not reparsed.
-;;
-;; tests wanted:
-;; - unlock checks for ancestors of failed jobs in different cases
-;; - two require jobs, where the first finishes, while the second is
-;;   in a state before waiting-dep
-;; - a job depending on a failed dependee, where the dependee has been finished before
-;; - coq-par-create-file-job detects a dependency cycle
-;; - coq-par-create-file-job finds a job in every possible state
-;; - coq-par-create-file-job finds a failed job
-;; - all tests in all quick and all vos variants
 
 ;;; Code:
 
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index 1a006c11..1cc04880 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.el
@@ -720,7 +720,7 @@ modification time stamps and .vo and .vio are older than the
 dependency.
 
 Elements 2-4 of a test specify the results and side effects of
-`coq-par-job-needs-compilation' for all setting of
+`coq-par-job-needs-compilation' for all settings of
 `coq-compile-quick' on the file configuration described in
 element 1. The options `quick-no-vio2vo' and `quick-and-vio2vo'
 are specified together with label `quick'.  Each result and side