diff options
| -rw-r--r-- | theories/Reals/Reals.v | 1 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt.v | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index 43f8d03989..b50939f40b 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -33,6 +33,7 @@ Require Export Ranalysis. Require Export Rtopology. Require Export TAF. Require Export NewtonInt. +Require Export RiemannInt. Require Export DiscrR. Require Export SplitRmult. Require Export SplitAbsolu. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 58e953eb74..316af925be 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -24,7 +24,7 @@ Require Ranalysis4. Require Exp_prop. Require Rtopology. Require NewtonInt. -Require RiemannInt_SF. +Require Export RiemannInt_SF. Require Classical_Pred_Type. Require Max. |