Skip to content

Commit

Permalink
removing files not in mathcomp-1.6
Browse files Browse the repository at this point in the history
  • Loading branch information
Enrico Tassi committed Dec 11, 2015
1 parent 353eb61 commit 2042765
Show file tree
Hide file tree
Showing 133 changed files with 0 additions and 58,498 deletions.
90 changes: 0 additions & 90 deletions mathcomp/Make
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
algebra/all_algebra.v
algebra/finalg.v
algebra/fraction.v
algebra/intdiv.v
algebra/interval.v
algebra/matrix.v
Expand All @@ -16,7 +15,6 @@ algebra/ssrint.v
algebra/ssrnum.v
algebra/vector.v
algebra/zmodp.v
all/all.v
character/all_character.v
character/character.v
character/classfun.v
Expand All @@ -34,7 +32,6 @@ field/countalg.v
field/cyclotomic.v
field/falgebra.v
field/fieldext.v
field/finfield.v
field/galois.v
field/separable.v
fingroup/action.v
Expand All @@ -46,55 +43,9 @@ 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
Expand Down Expand Up @@ -131,47 +82,6 @@ ssreflect/ssrfun.v
ssreflect/ssrmatching.v
ssreflect/ssrnat.v
ssreflect/tuple.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
Expand Down
1 change: 0 additions & 1 deletion mathcomp/algebra/Make
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
all_algebra.v
finalg.v
fraction.v
intdiv.v
interval.v
matrix.v
Expand Down
1 change: 0 additions & 1 deletion mathcomp/algebra/all_algebra.v
Original file line number Diff line number Diff line change
Expand Up @@ -13,4 +13,3 @@ Require Export mxpoly.
Require Export mxalgebra.
Require Export vector.
Require Export ring_quotient.
Require Export fraction.
Loading

0 comments on commit 2042765

Please sign in to comment.