aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--mathcomp/algebra/Makefile8
-rw-r--r--mathcomp/all/Makefile22
-rw-r--r--mathcomp/character/Makefile7
-rw-r--r--mathcomp/field/Makefile7
-rw-r--r--mathcomp/fingroup/Makefile7
-rw-r--r--mathcomp/solvable/Makefile7
6 files changed, 12 insertions, 46 deletions
diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile
index 47dd8b4..23d9c98 100644
--- a/mathcomp/algebra/Makefile
+++ b/mathcomp/algebra/Makefile
@@ -1,10 +1,6 @@
# -*- Makefile -*-
-COQPROJECT="Make"
-
-# --------------------------------------------------------------------
-include ../Makefile.common
-
-# --------------------------------------------------------------------
+COQPROJECT=Make
COQMAKEOPTIONS=--no-print-directory
+include ../Makefile.common
diff --git a/mathcomp/all/Makefile b/mathcomp/all/Makefile
index 30204d2..7e434c0 100644
--- a/mathcomp/all/Makefile
+++ b/mathcomp/all/Makefile
@@ -1,25 +1,7 @@
# -*- Makefile -*-
-COQPROJECT="Make"
-
-# --------------------------------------------------------------------
-include Makefile.common
-
-# --------------------------------------------------------------------
+COQPROJECT=Make
COQMAKEOPTIONS=--no-print-directory
# --------------------------------------------------------------------
-.PHONY: install
-
-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)}'
-
+include ../Makefile.common
diff --git a/mathcomp/character/Makefile b/mathcomp/character/Makefile
index 47dd8b4..7e434c0 100644
--- a/mathcomp/character/Makefile
+++ b/mathcomp/character/Makefile
@@ -1,10 +1,7 @@
# -*- Makefile -*-
-COQPROJECT="Make"
+COQPROJECT=Make
+COQMAKEOPTIONS=--no-print-directory
# --------------------------------------------------------------------
include ../Makefile.common
-
-# --------------------------------------------------------------------
-COQMAKEOPTIONS=--no-print-directory
-
diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile
index 47dd8b4..7e434c0 100644
--- a/mathcomp/field/Makefile
+++ b/mathcomp/field/Makefile
@@ -1,10 +1,7 @@
# -*- Makefile -*-
-COQPROJECT="Make"
+COQPROJECT=Make
+COQMAKEOPTIONS=--no-print-directory
# --------------------------------------------------------------------
include ../Makefile.common
-
-# --------------------------------------------------------------------
-COQMAKEOPTIONS=--no-print-directory
-
diff --git a/mathcomp/fingroup/Makefile b/mathcomp/fingroup/Makefile
index 47dd8b4..7e434c0 100644
--- a/mathcomp/fingroup/Makefile
+++ b/mathcomp/fingroup/Makefile
@@ -1,10 +1,7 @@
# -*- Makefile -*-
-COQPROJECT="Make"
+COQPROJECT=Make
+COQMAKEOPTIONS=--no-print-directory
# --------------------------------------------------------------------
include ../Makefile.common
-
-# --------------------------------------------------------------------
-COQMAKEOPTIONS=--no-print-directory
-
diff --git a/mathcomp/solvable/Makefile b/mathcomp/solvable/Makefile
index 47dd8b4..7e434c0 100644
--- a/mathcomp/solvable/Makefile
+++ b/mathcomp/solvable/Makefile
@@ -1,10 +1,7 @@
# -*- Makefile -*-
-COQPROJECT="Make"
+COQPROJECT=Make
+COQMAKEOPTIONS=--no-print-directory
# --------------------------------------------------------------------
include ../Makefile.common
-
-# --------------------------------------------------------------------
-COQMAKEOPTIONS=--no-print-directory
-