1 files changed, 37 insertions, 0 deletions
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