aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-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 8631841fb1..080f2a4c2f 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.