improve compilation when both .vio and .vo are up-to-date

In this case Coq loads the younger file and emits a warning if
the .vio file is the younger one. With this patch, the dependency
analysis for parallel compilation continues with the older value.
The interesting case to look at is when b.v depends on a.v and
both are compiled with -quick and later a parallel vio2vo
produces a.vo and b.vo such that b.vo is older (because, eg. b.v
is shorter than a.v). Without this patch a second auto
compilation would recompile b.v, because the dependency a.vo is
younger.

1 files changed, 4 insertions, 3 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 1840f9a0..910fbd7e 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -389,9 +389,10 @@ modules are matched separately with `coq-require-id-regexp'")
 
 (defun time-less-or-equal (time-1 time-2)
   "Return `t' if time value time-1 is earlier or equal to time-2.
-A time value is a list of two integers as returned by `file-attributes'.
-The first integer contains the upper 16 bits and the second the lower
-16 bits of the time."
+A time value is a list of two, three or four integers of the
+form (high low micro pico) as returned by `file-attributes' or
+'current-time'. First element high contains the upper 16 bits and
+the second low the lower 16 bits of the time."
   (not (time-less-p time-2 time-1)))
 
 (defun coq-max-dep-mod-time (dep-mod-times)