aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/EqualitiesFacts.v
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-01-13 17:38:27 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-01-13 17:38:27 +0100
commit4b4a4b6b41e6b303d556638ed2a79b1493b1ecf4 (patch)
tree5202a95f44355a5019680a6ae90a93fa169724d2 /theories/Structures/EqualitiesFacts.v
parent245affffb174fb26fc9a847abe44e01b107980a8 (diff)
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.
Diffstat (limited to 'theories/Structures/EqualitiesFacts.v')
-rw-r--r--theories/Structures/EqualitiesFacts.v2
1 files changed, 1 insertions, 1 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).