packaging odd_order

6 files changed, 53 insertions, 0 deletions

diff --git a/mathcomp/odd_order/AUTHORS b/mathcomp/odd_order/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/odd_order/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/odd_order/CeCILL-B b/mathcomp/odd_order/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/odd_order/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/odd_order/INSTALL b/mathcomp/odd_order/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/odd_order/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/odd_order/Make b/mathcomp/odd_order/Make
new file mode 100644
index 0000000..d7ed459
--- /dev/null
+++ b/mathcomp/odd_order/Make
@@ -0,0 +1,37 @@
+all.v
+BGappendixAB.v
+BGappendixC.v
+BGsection10.v
+BGsection11.v
+BGsection12.v
+BGsection13.v
+BGsection14.v
+BGsection15.v
+BGsection16.v
+BGsection1.v
+BGsection2.v
+BGsection3.v
+BGsection4.v
+BGsection5.v
+BGsection6.v
+BGsection7.v
+BGsection8.v
+BGsection9.v
+PFsection10.v
+PFsection11.v
+PFsection12.v
+PFsection13.v
+PFsection14.v
+PFsection1.v
+PFsection2.v
+PFsection3.v
+PFsection4.v
+PFsection5.v
+PFsection6.v
+PFsection7.v
+PFsection8.v
+PFsection9.v
+stripped_odd_order_theorem.v
+wielandt_fixpoint.v
+
+-R . mathcomp.odd_order
diff --git a/mathcomp/odd_order/README b/mathcomp/odd_order/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/odd_order/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/odd_order/opam b/mathcomp/odd_order/opam
new file mode 100644
index 0000000..bf978cd
--- /dev/null
+++ b/mathcomp/odd_order/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:odd_order"
+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/odd_order'" ]
+depends: [ "coq:mathcomp:character" { = "1.5" } ]