Merge branch 'v8.5'

3 files changed, 3 insertions, 3 deletions

diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index d5827d87a0..cee3d63f00 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).
 
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index b484257b99..89c5638828 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/OrdersLists.v b/theories/Structures/OrdersLists.v
index 41e65d7287..bf8529bc79 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 *)