packaging fingroup and algebra

The files zmodp and cyclic in fingroup had dependecies in algebra so I put them there.
I'm not convinced it's the best solution to this problem.
Maybe more subdivisions in algebra would bring a better solution?

(Maybe we should send the whole problem to a solver? :P)

19 files changed, 121 insertions, 12 deletions

diff --git a/mathcomp/algebra/AUTHORS b/mathcomp/algebra/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/algebra/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/algebra/CeCILL-B b/mathcomp/algebra/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/algebra/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/algebra/INSTALL b/mathcomp/algebra/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/algebra/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make
new file mode 100644
index 0000000..d9f4c63
--- /dev/null
+++ b/mathcomp/algebra/Make
@@ -0,0 +1,21 @@
+all.v
+finalg.v
+fraction.v
+intdiv.v
+interval.v
+matrix.v
+mxalgebra.v
+mxpoly.v
+polydiv.v
+poly.v
+polyXY.v
+rat.v
+ring_quotient.v
+ssralg.v
+ssrint.v
+ssrnum.v
+vector.v
+zmodp.v
+cyclic.v
+
+-R . mathcomp.algebra
diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile
new file mode 100644
index 0000000..d693257
--- /dev/null
+++ b/mathcomp/algebra/Makefile
@@ -0,0 +1,23 @@
+H=@
+
+ifeq "$(COQBIN)" ""
+COQBIN=$(dir $(shell which coqtop))/
+endif
+
+
+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 $*
+
+.PHONY: clean
+clean:
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq clean
+	$(H)rm -f Makefile.coq
+
diff --git a/mathcomp/algebra/README b/mathcomp/algebra/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/algebra/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/algebra/all.v b/mathcomp/algebra/all.v
index f4406a9..8a93ca9 100644
--- a/mathcomp/algebra/all.v
+++ b/mathcomp/algebra/all.v
@@ -1,16 +1,16 @@
+Require Export ssralg.
+Require Export ssrnum.
 Require Export finalg.
-Require Export fraction.
+Require Export poly.
+Require Export polydiv.
+Require Export polyXY.
+Require Export ssrint.
+Require Export rat.
 Require Export intdiv.
 Require Export interval.
 Require Export matrix.
-Require Export mxalgebra.
 Require Export mxpoly.
-Require Export polydiv.
-Require Export poly.
-Require Export polyXY.
-Require Export rat.
-Require Export ring_quotient.
-Require Export ssralg.
-Require Export ssrint.
-Require Export ssrnum.
+Require Export mxalgebra.
 Require Export vector.
+Require Export ring_quotient.
+Require Export fraction.
diff --git a/mathcomp/fingroup/cyclic.v b/mathcomp/algebra/cyclic.v
index ad10492..ad10492 100644
--- a/mathcomp/fingroup/cyclic.v
+++ b/mathcomp/algebra/cyclic.v
diff --git a/mathcomp/algebra/opam b/mathcomp/algebra/opam
new file mode 100644
index 0000000..f662b48
--- /dev/null
+++ b/mathcomp/algebra/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:algebra"
+version: "1.5"
+maintainer: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+authors: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+homepage: "http://ssr.msr-inria.inria.fr/"
+bug-reports: "ssreflect@msr-inria.inria.fr"
+license: "CeCILL-B"
+build: [ make "-j" "%{jobs}%" ] 
+install: [ make "install" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/algebra'" ]
+depends: [ "coq:mathcomp:fingroup" { = "1.5" } ]
diff --git a/mathcomp/fingroup/zmodp.v b/mathcomp/algebra/zmodp.v
index df5b378..df5b378 100644
--- a/mathcomp/fingroup/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
diff --git a/mathcomp/all.v b/mathcomp/all/all.v
index 9be65b2..9be65b2 100644
--- a/mathcomp/all.v
+++ b/mathcomp/all/all.v
diff --git a/mathcomp/fingroup/AUTHORS b/mathcomp/fingroup/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/fingroup/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/fingroup/CeCILL-B b/mathcomp/fingroup/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/fingroup/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/fingroup/INSTALL b/mathcomp/fingroup/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/fingroup/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/fingroup/Make b/mathcomp/fingroup/Make
new file mode 100644
index 0000000..ece5714
--- /dev/null
+++ b/mathcomp/fingroup/Make
@@ -0,0 +1,11 @@
+action.v
+all.v
+automorphism.v
+fingroup.v
+gproduct.v
+morphism.v
+perm.v
+presentation.v
+quotient.v
+
+-R . mathcomp.fingroup
diff --git a/mathcomp/fingroup/Makefile b/mathcomp/fingroup/Makefile
new file mode 100644
index 0000000..d693257
--- /dev/null
+++ b/mathcomp/fingroup/Makefile
@@ -0,0 +1,23 @@
+H=@
+
+ifeq "$(COQBIN)" ""
+COQBIN=$(dir $(shell which coqtop))/
+endif
+
+
+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 $*
+
+.PHONY: clean
+clean:
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq clean
+	$(H)rm -f Makefile.coq
+
diff --git a/mathcomp/fingroup/README b/mathcomp/fingroup/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/fingroup/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/fingroup/all.v b/mathcomp/fingroup/all.v
index 0cf8995..903da3c 100644
--- a/mathcomp/fingroup/all.v
+++ b/mathcomp/fingroup/all.v
@@ -1,10 +1,9 @@
 Require Export action.
 Require Export automorphism.
-Require Export cyclic.
 Require Export fingroup.
 Require Export gproduct.
 Require Export morphism.
 Require Export perm.
 Require Export presentation.
 Require Export quotient.
-Require Export zmodp.
+
diff --git a/mathcomp/fingroup/opam b/mathcomp/fingroup/opam
new file mode 100644
index 0000000..4a46943
--- /dev/null
+++ b/mathcomp/fingroup/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:fingroup"
+version: "1.5"
+maintainer: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+authors: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+homepage: "http://ssr.msr-inria.inria.fr/"
+bug-reports: "ssreflect@msr-inria.inria.fr"
+license: "CeCILL-B"
+build: [ make "-j" "%{jobs}%" ] 
+install: [ make "install" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/fingroup'" ]
+depends: [ "coq:mathcomp:discrete" { = "1.5" } ]