Updating files + reorganizing everything

1 files changed, 182 insertions, 0 deletions

diff --git a/mathcomp/Make b/mathcomp/Make
new file mode 100644
index 0000000..d8fb252
--- /dev/null
+++ b/mathcomp/Make
@@ -0,0 +1,182 @@
+algebra/all_algebra.v
+algebra/finalg.v
+algebra/fraction.v
+algebra/intdiv.v
+algebra/interval.v
+algebra/matrix.v
+algebra/mxalgebra.v
+algebra/mxpoly.v
+algebra/polydiv.v
+algebra/poly.v
+algebra/polyXY.v
+algebra/rat.v
+algebra/ring_quotient.v
+algebra/ssralg.v
+algebra/ssrint.v
+algebra/ssrnum.v
+algebra/vector.v
+algebra/zmodp.v
+all/all.v
+basic/all_basic.v
+basic/bigop.v
+basic/binomial.v
+basic/choice.v
+basic/div.v
+basic/finfun.v
+basic/fingraph.v
+basic/finset.v
+basic/fintype.v
+basic/generic_quotient.v
+basic/path.v
+basic/prime.v
+basic/tuple.v
+character/all_character.v
+character/character.v
+character/classfun.v
+character/finfield.v
+character/inertia.v
+character/integral_char.v
+character/mxabelem.v
+character/mxrepresentation.v
+character/vcharacter.v
+field/algC.v
+field/algebraics_fundamentals.v
+field/algnum.v
+field/all_field.v
+field/closed_field.v
+field/countalg.v
+field/cyclotomic.v
+field/falgebra.v
+field/fieldext.v
+field/galois.v
+field/separable.v
+fingroup/action.v
+fingroup/all_fingroup.v
+fingroup/automorphism.v
+fingroup/fingroup.v
+fingroup/gproduct.v
+fingroup/morphism.v
+fingroup/perm.v
+fingroup/presentation.v
+fingroup/quotient.v
+odd_order/BGappendixAB.v
+odd_order/BGappendixC.v
+odd_order/BGsection10.v
+odd_order/BGsection11.v
+odd_order/BGsection12.v
+odd_order/BGsection13.v
+odd_order/BGsection14.v
+odd_order/BGsection15.v
+odd_order/BGsection16.v
+odd_order/BGsection1.v
+odd_order/BGsection2.v
+odd_order/BGsection3.v
+odd_order/BGsection4.v
+odd_order/BGsection5.v
+odd_order/BGsection6.v
+odd_order/BGsection7.v
+odd_order/BGsection8.v
+odd_order/BGsection9.v
+odd_order/PFsection10.v
+odd_order/PFsection11.v
+odd_order/PFsection12.v
+odd_order/PFsection13.v
+odd_order/PFsection14.v
+odd_order/PFsection1.v
+odd_order/PFsection2.v
+odd_order/PFsection3.v
+odd_order/PFsection4.v
+odd_order/PFsection5.v
+odd_order/PFsection6.v
+odd_order/PFsection7.v
+odd_order/PFsection8.v
+odd_order/PFsection9.v
+odd_order/stripped_odd_order_theorem.v
+odd_order/wielandt_fixpoint.v
+real_closed/all_real_closed.v
+real_closed/bigenough.v
+real_closed/cauchyreals.v
+real_closed/complex.v
+real_closed/mxtens.v
+real_closed/ordered_qelim.v
+real_closed/polyorder.v
+real_closed/polyrcf.v
+real_closed/qe_rcf_th.v
+real_closed/qe_rcf.v
+real_closed/realalg.v
+solvable/abelian.v
+solvable/all_solvable.v
+solvable/alt.v
+solvable/burnside_app.v
+solvable/center.v
+solvable/commutator.v
+solvable/cyclic.v
+solvable/extraspecial.v
+solvable/extremal.v
+solvable/finmodule.v
+solvable/frobenius.v
+solvable/gfunctor.v
+solvable/gseries.v
+solvable/hall.v
+solvable/jordanholder.v
+solvable/maximal.v
+solvable/nilpotent.v
+solvable/pgroup.v
+solvable/primitive_action.v
+solvable/sylow.v
+ssreflect/all_ssreflect.v
+ssreflect/eqtype.v
+ssreflect/seq.v
+ssreflect/ssrbool.v
+ssreflect/ssreflect.v
+ssreflect/ssrfun.v
+ssreflect/ssrmatching.v
+ssreflect/ssrnat.v
+ssrtest/absevarprop.v
+ssrtest/binders_of.v
+ssrtest/binders.v
+ssrtest/caseview.v
+ssrtest/congr.v
+ssrtest/deferclear.v
+ssrtest/dependent_type_err.v
+ssrtest/elim2.v
+ssrtest/elim_pattern.v
+ssrtest/elim.v
+ssrtest/first_n.v
+ssrtest/gen_have.v
+ssrtest/gen_pattern.v
+ssrtest/havesuff.v
+ssrtest/have_TC.v
+ssrtest/have_transp.v
+ssrtest/have_view_idiom.v
+ssrtest/if_isnt.v
+ssrtest/indetLHS.v
+ssrtest/intro_beta.v
+ssrtest/intro_noop.v
+ssrtest/ipatalternation.v
+ssrtest/ltac_have.v
+ssrtest/ltac_in.v
+ssrtest/move_after.v
+ssrtest/multiview.v
+ssrtest/occarrow.v
+ssrtest/patnoX.v
+ssrtest/rewpatterns.v
+ssrtest/set_lamda.v
+ssrtest/set_pattern.v
+ssrtest/ssrsyntax1.v
+ssrtest/ssrsyntax2.v
+ssrtest/tc.v
+ssrtest/testmx.v
+ssrtest/typeof.v
+ssrtest/unkeyed.v
+ssrtest/view_case.v
+ssrtest/wlogletin.v
+ssrtest/wlog_suff.v
+ssrtest/wlong_intro.v
+ssreflect.ml4
+ssreflect.mllib
+ssrmatching.ml4
+ssrmatching.mli
+
+-I .
+-R . mathcomp