aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authordesmettr2002-09-25 17:26:54 +0000
committerdesmettr2002-09-25 17:26:54 +0000
commit5416c30a6f7b9b5f603cdfdd5b1cf5049620559f (patch)
tree16dd357b5ddcee34b593de5a12298dc8a50307e5
parent62712cda8380f03c6d60c5987f9ff08b866127a8 (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3033 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 97c9b1d1bd..460b36d6ed 100644
--- a/Makefile
+++ b/Makefile
@@ -532,7 +532,7 @@ REALSVO=theories/Reals/TypeSyntax.vo \
theories/Reals/Cauchy_prod.vo theories/Reals/Cv_prop.vo \
theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo \
theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo \
- theories/Reals/TAF.vo \
+ theories/Reals/Rtopology.vo theories/Reals/TAF.vo \
theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo \
theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo \
theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo \