5 files changed, 7 insertions, 7 deletions
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index 8e2b2d08..cee3d63f 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -10,7 +10,7 @@ Require Import Equalities Bool SetoidList RelationPairs.
 
 Set Implicit Arguments.
 
-(** * Keys and datas used in MMap *)
+(** * Keys and datas used in the future MMaps *)
 
 Module KeyDecidableType(D:DecidableType).
 
@@ -60,7 +60,7 @@ Module KeyDecidableType(D:DecidableType).
 
  Hint Resolve eqke_1 eqke_2 eqk_1.
 
- (* Additionnal facts *)
+ (* Additional facts *)
 
  Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) :
    InA eqke p m -> InA eqk p m.
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.
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index b484257b..89c56388 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -87,7 +87,7 @@ End PairOrderedType.
 (** Even if [positive] can be seen as an ordered type with respect to the
   usual order (see above), we can also use a lexicographic order over bits
   (lower bits are considered first). This is more natural when using
-  [positive] as indexes for sets or maps (see MSetPositive and MMapPositive. *)
+  [positive] as indexes for sets or maps (see MSetPositive). *)
 
 Local Open Scope positive.
 
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 88fbd8c1..954d3df2 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -90,7 +90,7 @@ Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull').
  Instance le_order : PartialOrder eq le.
  Proof. compute; iorder. Qed.
 
- Instance le_antisym : Antisymmetric eq le.
+ Instance le_antisym : Antisymmetric _ eq le.
  Proof. apply partial_order_antisym; auto with *. Qed.
 
  Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 4d49ac84..bf8529bc 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -54,7 +54,7 @@ Hint Immediate In_eq Inf_lt.
 End OrderedTypeLists.
 
 
-(** * Results about keys and data as manipulated in MMaps. *)
+(** * Results about keys and data as manipulated in the future MMaps. *)
 
 Module KeyOrderedType(O:OrderedType).
  Include KeyDecidableType(O). (* provides eqk, eqke *)
@@ -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.