packaging real_closed

1 files changed, 13 insertions, 0 deletions

diff --git a/mathcomp/real_closed/Make b/mathcomp/real_closed/Make
new file mode 100644
index 0000000..08eedc2
--- /dev/null
+++ b/mathcomp/real_closed/Make
@@ -0,0 +1,13 @@
+-R . mathcomp.real_closed
+
+all.v
+bigenough.v
+cauchyreals.v
+complex.v
+ordered_qelim.v
+polyorder.v
+polyrcf.v
+qe_rcf_th.v
+qe_rcf.v
+realalg.v
+mxtens.v
\ No newline at end of file