aboutsummaryrefslogtreecommitdiff
path: root/theories/MSets/MSetProperties.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets/MSetProperties.v')
-rw-r--r--theories/MSets/MSetProperties.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index dc82a14502..a9ba0a823b 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -17,7 +17,7 @@
[Equal s s'] instead of [equal s s'=true], etc. *)
Require Export MSetInterface.
-Require Import DecidableTypeEx OrderedType2Lists MSetFacts MSetDecide.
+Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide.
Set Implicit Arguments.
Unset Strict Implicit.