summaryrefslogtreecommitdiff
path: root/theories/Reals/vo.itarget
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/vo.itarget')
-rw-r--r--theories/Reals/vo.itarget1
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Reals/vo.itarget b/theories/Reals/vo.itarget
index 36dd0f56..0c8f0b97 100644
--- a/theories/Reals/vo.itarget
+++ b/theories/Reals/vo.itarget
@@ -8,7 +8,6 @@ Cos_rel.vo
DiscrR.vo
Exp_prop.vo
Integration.vo
-LegacyRfield.vo
Machin.vo
MVT.vo
NewtonInt.vo