summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
commit164c6861860e6b52818c031f901ffeff91fca16a (patch)
tree4f91d20c890c25915e7b28226c663b94a8cfb0d3 /doc
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'doc')
-rw-r--r--doc/stdlib/index-list.html.template8
1 files changed, 1 insertions, 7 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 866193ff..d6b1af79 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>:
@@ -617,6 +610,7 @@ through the <tt>Require Import</tt> command.</p>
Compatibility wrappers for previous versions of Coq
</dt>
<dd>
+ theories/Compat/AdmitAxiom.v
theories/Compat/Coq84.v
theories/Compat/Coq85.v
</dd>