From e2530e78deda5cf6be2111951efb8ea747af7fa8 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 2 Apr 2015 13:31:52 +0200
Subject: Broken global Makefile

---
 mathcomp/Makefile    | 37 +++++++++++++++++++++++++++++++++++++
 mathcomp/_CoqProject |  1 +
 2 files changed, 38 insertions(+)
 create mode 100644 mathcomp/Makefile
 create mode 100644 mathcomp/_CoqProject

diff --git a/mathcomp/Makefile b/mathcomp/Makefile
new file mode 100644
index 0000000..dcd5f4e
--- /dev/null
+++ b/mathcomp/Makefile
@@ -0,0 +1,37 @@
+
+.PHONY: ssreflect algebra fingroup all odd_order solvable field character discrete real_closed ssrtest
+
+export COQPATH=$(PWD)/..
+
+all: ssreflect algebra fingroup odd_order solvable field character discrete real_closed ssrtest
+	$(MAKE) -C $@
+
+ssrefect:
+	$(MAKE) -C $@
+
+algebra: fingroup
+	$(MAKE) -C $@
+
+fingroup: discrete
+	$(MAKE) -C $@
+
+odd_order: field
+	$(MAKE) -C $@
+
+solvable: algebra
+	$(MAKE) -C $@
+
+field: solvable
+	$(MAKE) -C $@
+
+character: field
+	$(MAKE) -C $@
+
+discrete: ssreflect
+	$(MAKE) -C $@
+
+real_closed: algebra
+	$(MAKE) -C $@
+
+ssrtest: algebra
+	$(MAKE) -C $@
diff --git a/mathcomp/_CoqProject b/mathcomp/_CoqProject
new file mode 100644
index 0000000..9e1621c
--- /dev/null
+++ b/mathcomp/_CoqProject
@@ -0,0 +1 @@
+-R . mathcomp
\ No newline at end of file
-- 
cgit v1.2.3