aboutsummaryrefslogtreecommitdiff
path: root/theories/MSets/MSets.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets/MSets.v')
-rw-r--r--theories/MSets/MSets.v9
1 files changed, 4 insertions, 5 deletions
diff --git a/theories/MSets/MSets.v b/theories/MSets/MSets.v
index 42966c7fc2..558b09562d 100644
--- a/theories/MSets/MSets.v
+++ b/theories/MSets/MSets.v
@@ -8,11 +8,10 @@
(* $Id$ *)
-Require Export OrderedType2.
-Require Export OrderedType2Ex.
-Require Export OrderedType2Alt.
-Require Export DecidableType2.
-Require Export DecidableType2Ex.
+Require Export Orders.
+Require Export OrdersEx.
+Require Export OrdersAlt.
+Require Export Equalities.
Require Export MSetInterface.
Require Export MSetFacts.
Require Export MSetDecide.