aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSets.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSets.v')
-rw-r--r--theories/FSets/FSets.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v
index 51cd23c12..8b4123ebd 100644
--- a/theories/FSets/FSets.v
+++ b/theories/FSets/FSets.v
@@ -9,8 +9,11 @@
(* $Id$ *)
Require Export OrderedType.
+Require Export OrderedTypeEx.
+Require Export OrderedTypeAlt.
Require Export FSetInterface.
Require Export FSetBridge.
Require Export FSetProperties.
Require Export FSetEqProperties.
Require Export FSetList.
+Require Export FSetToFiniteSet. \ No newline at end of file