aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-06-13 12:36:03 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-06-13 12:36:03 +0000
commit75bfb5b76eafb1b73fac2d792961f28d60a8251a (patch)
treeaa701a63e3fea55b7993cd956489797ea10d54d1
parenta2607747e6e6a521e43da29f6c14dc81b1c96978 (diff)
Require Export
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4152 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--theories/FSets/FSet.v10
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/FSets/FSet.v b/theories/FSets/FSet.v
index 50f3799ed..66009e3ac 100644
--- a/theories/FSets/FSet.v
+++ b/theories/FSets/FSet.v
@@ -8,9 +8,9 @@
(* $Id$ *)
-Require FSetInterface.
-Require FSetBridge.
-Require FSetProperties.
-Require FSetList.
-Require FSetRBT.
+Require Export FSetInterface.
+Require Export FSetBridge.
+Require Export FSetProperties.
+Require Export FSetList.
+Require Export FSetRBT.