10 files changed, 157 insertions, 164 deletions
diff --git a/mathcomp/Makefile b/mathcomp/Makefile
index 07f1869..efc2ff8 100644
--- a/mathcomp/Makefile
+++ b/mathcomp/Makefile
@@ -1,30 +1,23 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
+# --------------------------------------------------------------------
 # this sets variable V
 include ssreflect/Makefile.detect-coq-version
-# this defined coqmakefile
+# this defines prepare_coqmakefile
 include ssreflect/Makefile.coq-makefile
+include Makefile.common
 
-COQDEP=$(COQBIN)coqdep
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory \
+	COQDEP='$(COQDEP) -exclude-dir ssreflect/plugin -c'
+COQMAKEFILEOPTIONS=$(MLLIB) $(EXTRA)
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
+# --------------------------------------------------------------------
+.PHONY: pre_makefile
+BEFOREMAKEFILE=pre_makefile
 
-.DEFAULT_GOAL := all
+pre_makefile:
+	$(call prepare_coqmakefile,ssreflect)
 
-%:
-	$(H)[ -e Makefile.coq ] || $(call coqmakefile,ssreflect)
-	# Override COQDEP to find only the "right" copy .ml files
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -exclude-dir plugin -c'
-
-clean: 
-	$(H)[ -e Makefile.coq ] || $(call coqmakefile,ssreflect)
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
new file mode 100644
index 0000000..b07b78d
--- /dev/null
+++ b/mathcomp/Makefile.common
@@ -0,0 +1,78 @@
+# -*- Makefile -*-
+
+ifeq "$(COQBIN)" ""
+COQBIN=$(dir $(shell which coqtop))/
+endif
+ifeq "$(COQMAKEFILE)" ""
+COQMAKEFILE=$(COQBIN)coq_makefile
+endif
+COQDEP=$(COQBIN)coqdep
+
+ifeq "$(COQPROJECT)" ""
+COQPROJECT="_CoqProject"
+endif
+
+# --------------------------------------------------------------------
+.PHONY: all config build clean distclean __always__
+.SUFFIXES:
+
+TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
+COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
+
+# --------------------------------------------------------------------
+all: config build
+
+# --------------------------------------------------------------------
+Makefile.coq: Makefile $(BEFOREMAKEFILE)
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
+
+# --------------------------------------------------------------------
+config: sub-config this-config Makefile.coq
+
+build: sub-build this-build
+
+clean: sub-clean this-clean
+
+distclean: sub-distclean this-distclean
+
+# --------------------------------------------------------------------
+.PHONY: this-config this-build this-distclean this-clean
+
+this-build::
+	+$(COQMAKE)
+
+this-distclean:: this-clean
+	rm -f Makefile.coq Makefile.coq.conf
+
+this-clean::
+	@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
+
+# --------------------------------------------------------------------
+.PHONY: install
+
+install:
+	$(COQMAKE) install
+# --------------------------------------------------------------------
+.PHONY: count
+
+COQFILES := $(shell grep '.v$$' Make)
+
+count:
+	@coqwc $(COQFILES) | tail -1 | \
+	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
+# --------------------------------------------------------------------
+this-distclean::
+	rm -f $(shell find . -name '*~')
+
+# --------------------------------------------------------------------
+ifdef SUBDIRS
+sub-%: __always__
+	@set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done
+else
+sub-%: __always__
+	@true
+endif
+
+# --------------------------------------------------------------------
+%.vo: __always__
+	+$(COQMAKE) $@
diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile
index d4e1bca..47dd8b4 100644
--- a/mathcomp/algebra/Makefile
+++ b/mathcomp/algebra/Makefile
@@ -1,24 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/all/Makefile b/mathcomp/all/Makefile
index a58be7b..30204d2 100644
--- a/mathcomp/all/Makefile
+++ b/mathcomp/all/Makefile
@@ -1,22 +1,25 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
+# --------------------------------------------------------------------
+include Makefile.common
 
-.DEFAULT_GOAL := all
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+# --------------------------------------------------------------------
+.PHONY: install
 
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+install:
+	$(MAKE) -f Makefile.coq install
+
+# --------------------------------------------------------------------
+.PHONY: count
+
+COQFILES := $(shell grep '.v$$' Make)
+
+count:
+	@coqwc $(COQFILES) | tail -1 | \
+	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
 
diff --git a/mathcomp/character/Makefile b/mathcomp/character/Makefile
index 14acb5c..47dd8b4 100644
--- a/mathcomp/character/Makefile
+++ b/mathcomp/character/Makefile
@@ -1,25 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile
index 14acb5c..47dd8b4 100644
--- a/mathcomp/field/Makefile
+++ b/mathcomp/field/Makefile
@@ -1,25 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/fingroup/Makefile b/mathcomp/fingroup/Makefile
index 14acb5c..47dd8b4 100644
--- a/mathcomp/fingroup/Makefile
+++ b/mathcomp/fingroup/Makefile
@@ -1,25 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/solvable/Makefile b/mathcomp/solvable/Makefile
index 14acb5c..47dd8b4 100644
--- a/mathcomp/solvable/Makefile
+++ b/mathcomp/solvable/Makefile
@@ -1,25 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile
index e4474c2..817a89c 100644
--- a/mathcomp/ssreflect/Makefile
+++ b/mathcomp/ssreflect/Makefile
@@ -1,28 +1,22 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
+# --------------------------------------------------------------------
 # this sets variable V
 include Makefile.detect-coq-version
-# this defined coqmakefile
+# this defines prepare_coqmakefile
 include Makefile.coq-makefile
+include ../Makefile.common
 
-COQDEP=$(COQBIN)coqdep
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory \
+	COQDEP='$(COQDEP) -exclude-dir plugin -c'
+COQMAKEFILEOPTIONS=$(MLLIB) $(EXTRA)
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
+# --------------------------------------------------------------------
+.PHONY: pre_makefile
+BEFOREMAKEFILE=pre_makefile
 
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(call coqmakefile,.)
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -exclude-dir plugin -c'
-
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+pre_makefile:
+	$(call prepare_coqmakefile,.)
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile
index ba0e5d7..e904236 100644
--- a/mathcomp/ssreflect/Makefile.coq-makefile
+++ b/mathcomp/ssreflect/Makefile.coq-makefile
@@ -1,4 +1,4 @@
-define coqmakefile
+define prepare_coqmakefile
 	(echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\
 	if [ "$$OS" = "Windows_NT" ]; then LN=cp; else LN="ln -sfr"; fi;\
 	MLLIB=;\
@@ -26,7 +26,6 @@ define coqmakefile
 		MLLIB=ssreflect_plugin.mlpack;\
 		EXTRA="ssreflect.ml4";\
 	;;\
-	esac;\
-	$(COQBIN)coq_makefile -f Make $$MLLIB $$EXTRA -o Makefile.coq)
+	esac
 endef