From 13479422b0286c86d0888e06aba112153ca6314d Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 17 Apr 2018 17:00:15 +0200
Subject: Moving real_closed to another repo

---
 mathcomp/Make | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'mathcomp/Make')

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
-- 
cgit v1.2.3