MMaps: remove it from final 8.5 release, since this new library isn't mature enough

 In particular, its interface might still change (in interaction with interested
 colleagues). So let's not give it too much visibility yet. Instead, I'll turn
 it as an opam packages for now.

3 files changed, 3 insertions, 3 deletions

diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index d5827d87a..cee3d63f0 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 b484257b9..89c563882 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 41e65d728..bf8529bc7 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 *)