From 4b4a4b6b41e6b303d556638ed2a79b1493b1ecf4 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 13 Jan 2016 17:38:27 +0100 Subject: 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. --- theories/Structures/EqualitiesFacts.v | 2 +- theories/Structures/OrdersEx.v | 2 +- theories/Structures/OrdersLists.v | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Structures') 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 *) -- cgit v1.2.3