aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FMapFacts.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FMapFacts.v')
-rw-r--r--theories/FSets/FMapFacts.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 7665ac05b..0c1448c9b 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -652,7 +652,7 @@ Add Relation key E.eq
transitivity proved by E.eq_trans
as KeySetoid.
-Implicit Arguments Equal [[elt]].
+Arguments Equal {elt} m m'.
Add Parametric Relation (elt : Type) : (t elt) Equal
reflexivity proved by (@Equal_refl elt)