summaryrefslogtreecommitdiff
path: root/theories/FSets/FMapFacts.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FMapFacts.v')
-rw-r--r--theories/FSets/FMapFacts.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index df12166e..d91eb87a 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *)
+(* $Id: FMapFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *)
(** * Finite maps library *)
@@ -15,7 +15,7 @@
different styles: equivalence and boolean equalities.
*)
-Require Import Bool DecidableType DecidableTypeEx OrderedType.
+Require Import Bool DecidableType DecidableTypeEx OrderedType Morphisms.
Require Export FMapInterface.
Set Implicit Arguments.
Unset Strict Implicit.