aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrdersLists.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures/OrdersLists.v')
-rw-r--r--theories/Structures/OrdersLists.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 4d49ac84e..41e65d728 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -76,7 +76,7 @@ Module KeyOrderedType(O:OrderedType).
Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt).
Proof. eapply subrelation_proper; eauto with *. Qed.
- (* Additionnal facts *)
+ (* Additional facts *)
Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt).
Proof. apply pair_compat. Qed.