Merge remote-tracking branch 'origin/pr/192'

1 files changed, 0 insertions, 36 deletions

diff --git a/mathcomp/odd_order/Make b/mathcomp/odd_order/Make
deleted file mode 100644
index a7ba4be..0000000
--- a/mathcomp/odd_order/Make
+++ /dev/null
@@ -1,36 +0,0 @@
-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