aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/real_closed/Make
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/real_closed/Make')
-rw-r--r--mathcomp/real_closed/Make13
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