aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-25 13:43:17 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-25 13:43:17 +0000
commit20ae362885ce40d5b81526aee0dc96a3aabe2cee (patch)
treeef187e9f16bb48d4156ffdaa456148f69046aae4 /theories/FSets
parent0def214a2e9fb473d0f137598d5ee38d36c47c86 (diff)
oups, ne chargeait pas les bons fichiers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9278 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FSetWeak.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FSetWeak.v b/theories/FSets/FSetWeak.v
index 8631841fb..080f2a4c2 100644
--- a/theories/FSets/FSetWeak.v
+++ b/theories/FSets/FSetWeak.v
@@ -11,6 +11,6 @@
Require Export DecidableType.
Require Export DecidableTypeEx.
Require Export FSetWeakInterface.
-Require Export FSetFacts.
-Require Export FSetProperties.
+Require Export FSetWeakFacts.
+Require Export FSetWeakProperties.
Require Export FSetWeakList.