aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures')
-rw-r--r--theories/Structures/EqualitiesFacts.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index b394cf48d..8e2b2d081 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -8,6 +8,8 @@
Require Import Equalities Bool SetoidList RelationPairs.
+Set Implicit Arguments.
+
(** * Keys and datas used in MMap *)
Module KeyDecidableType(D:DecidableType).