Sort entries in the TOC by dependencies

We inject a custom order of VFILES (vernacular files) when deferring
the invocation the "html" PHONY-target in the generated Coq Makefile,
that is ordered using the output of the "coqdep" utility.  This
ensures that the partial order induced by Require is respected in the
output of "toc.html", up to topological sorting.

Makefile

@@ -11,8 +11,23 @@ all: coq html
 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq all
 
+define GENCoqDoc
+BEGIN { RS="[[:space:]]"; FS=":" }			\
+{							\
+    dirname = $$1;					\
+    cmd = "coqdep -f _CoqProject -sort " dirname;	\
+    while ((cmd | getline) > 0) {			\
+        if ($$0 ~ "^" dirname && !seen[$$0]) {		\
+	    print $$0;					\
+            seen[$$0] = 1;				\
+        }						\
+    }							\
+    close(cmd);						\
+}
+endef
+
 html: Makefile.coq
-	$(MAKE) -f Makefile.coq html
+	VFILES="$(shell echo $(COMPONENTS) | awk '$(GENCoqDoc)')" $(MAKE) -e -f Makefile.coq html
 
 Makefile.coq: _CoqProject
 	coq_makefile -f $< -o $@ COQDOCEXTRAFLAGS = "--lib-name $(PROJNAME)"