metadata for solvable and field

15 files changed, 113 insertions, 0 deletions

diff --git a/mathcomp/field/AUTHORS b/mathcomp/field/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/field/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/field/CeCILL-B b/mathcomp/field/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/field/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/field/INSTALL b/mathcomp/field/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/field/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/field/Make b/mathcomp/field/Make
new file mode 100644
index 0000000..93ff57c
--- /dev/null
+++ b/mathcomp/field/Make
@@ -0,0 +1,14 @@
+all.v
+algC.v
+algebraics_fundamentals.v
+algnum.v
+closed_field.v
+countalg.v
+cyclotomic.v
+falgebra.v
+fieldext.v
+finfield.v
+galois.v
+separable.v
+
+-R . mathcomp.field
diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile
new file mode 100644
index 0000000..d693257
--- /dev/null
+++ b/mathcomp/field/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/field/README b/mathcomp/field/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/field/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/field/opam b/mathcomp/field/opam
new file mode 100644
index 0000000..659ad66
--- /dev/null
+++ b/mathcomp/field/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:field"
+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/field'" ]
+depends: [ "coq:mathcomp:solvable" { = "1.5" } ]
diff --git a/mathcomp/solvable/wielandt_fixpoint.v b/mathcomp/odd_order/wielandt_fixpoint.v
index beebc3d..beebc3d 100644
--- a/mathcomp/solvable/wielandt_fixpoint.v
+++ b/mathcomp/odd_order/wielandt_fixpoint.v
diff --git a/mathcomp/solvable/AUTHORS b/mathcomp/solvable/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/solvable/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/solvable/CeCILL-B b/mathcomp/solvable/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/solvable/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/solvable/INSTALL b/mathcomp/solvable/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/solvable/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/solvable/Make b/mathcomp/solvable/Make
new file mode 100644
index 0000000..41bd3e0
--- /dev/null
+++ b/mathcomp/solvable/Make
@@ -0,0 +1,21 @@
+abelian.v
+all.v
+alt.v
+burnside_app.v
+center.v
+commutator.v
+extraspecial.v
+extremal.v
+finmodule.v
+frobenius.v
+gfunctor.v
+gseries.v
+hall.v
+jordanholder.v
+maximal.v
+nilpotent.v
+pgroup.v
+primitive_action.v
+sylow.v
+
+-R . mathcomp.solvable
diff --git a/mathcomp/solvable/Makefile b/mathcomp/solvable/Makefile
new file mode 100644
index 0000000..d693257
--- /dev/null
+++ b/mathcomp/solvable/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/solvable/README b/mathcomp/solvable/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/solvable/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/solvable/opam b/mathcomp/solvable/opam
new file mode 100644
index 0000000..e950335
--- /dev/null
+++ b/mathcomp/solvable/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:solvable"
+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/solvable'" ]
+depends: [ "coq:mathcomp:algebra" { = "1.5" } ]