From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- theories/Structures/OrderedType.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Structures/OrderedType.v') diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index cc8c2261..93ca383b 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -342,7 +342,7 @@ Module KeyOrderedType(O:OrderedType). compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. Qed. - (* Additionnal facts *) + (* Additional facts *) Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. Proof. -- cgit v1.2.3