From a8071b664c39d19e52053fc1fae91e2d61d22874 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Tue, 26 Nov 2002 18:41:54 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3298 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Reals.v      | 1 +
 theories/Reals/RiemannInt.v | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

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.
 
-- 
cgit v1.2.3