Moving real_closed to another repo

1 files changed, 0 insertions, 11 deletions

diff --git a/mathcomp/Make b/mathcomp/Make
index 1db29ba..ac48fc2 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -80,17 +80,6 @@ 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