aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib/index-list.html.template
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-01-31 16:18:14 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-01-31 16:18:14 +0000
commite9b044630d2a8c183eb9551435624c0dfeec3b1a (patch)
treee1a50cfa99bb56cfc01519ebed9f4257879727e0 /doc/stdlib/index-list.html.template
parentf519a1f10531e2513014fa4bbee9431aa4546faa (diff)
index-list.html.template: add missing files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib/index-list.html.template')
-rw-r--r--doc/stdlib/index-list.html.template12
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 35c13f3b7..de4b6de94 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -68,6 +68,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Logic/Epsilon.v
theories/Logic/IndefiniteDescription.v
theories/Logic/FunctionalExtensionality.v
+ theories/Logic/ExtensionalityFacts.v
</dd>
<dt> <b>Structures</b>:
@@ -395,6 +396,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Classes/SetoidClass.v
theories/Classes/SetoidDec.v
theories/Classes/RelationPairs.v
+ theories/Classes/DecidableClass.v
</dd>
<dt> <b>Setoids</b>:
@@ -414,6 +416,16 @@ through the <tt>Require Import</tt> command.</p>
theories/Lists/ListTactics.v
</dd>
+ <dt> <b>Vectors</b>:
+ Dependent datastructures storing their length
+ </dt>
+ <dd>
+ theories/Vectors/Fin.v
+ theories/Vectors/VectorDef.v
+ theories/Vectors/VectorSpec.v
+ (theories/Vectors/Vector.v)
+ </dd>
+
<dt> <b>Sorting</b>:
Axiomatizations of sorts
</dt>