diff options
Diffstat (limited to 'theories/Reals/Ranalysis_reg.v')
| -rw-r--r-- | theories/Reals/Ranalysis_reg.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index cb6d57be84..e6b3f2e37b 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -24,7 +24,6 @@ Require Export Rsqrt_def. Require Export R_sqrt. Require Export Rtrigo_calc. Require Export Rgeom. -Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. |