aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
authorPierre Letouzey2016-01-13 17:38:27 +0100
committerPierre Letouzey2016-01-13 17:38:27 +0100
commit4b4a4b6b41e6b303d556638ed2a79b1493b1ecf4 (patch)
tree5202a95f44355a5019680a6ae90a93fa169724d2 /doc/stdlib
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 'doc/stdlib')
-rw-r--r--doc/stdlib/index-list.html.template7
1 files changed, 0 insertions, 7 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 292b2b36cc..d6b1af797f 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -476,13 +476,6 @@ through the <tt>Require Import</tt> command.</p>
theories/MSets/MSetPositive.v
theories/MSets/MSetToFiniteSet.v
(theories/MSets/MSets.v)
- theories/MMaps/MMapAVL.v
- theories/MMaps/MMapFacts.v
- theories/MMaps/MMapInterface.v
- theories/MMaps/MMapList.v
- theories/MMaps/MMapPositive.v
- theories/MMaps/MMapWeakList.v
- (theories/MMaps/MMaps.v)
</dd>
<dt> <b>FSets</b>: