diff options
Diffstat (limited to 'mathcomp/real_closed/Make')
| -rw-r--r-- | mathcomp/real_closed/Make | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/mathcomp/real_closed/Make b/mathcomp/real_closed/Make deleted file mode 100644 index 1e013d3..0000000 --- a/mathcomp/real_closed/Make +++ /dev/null @@ -1,13 +0,0 @@ -all_real_closed.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 - --R . mathcomp.real_closed
\ No newline at end of file |
