aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib/index-list.html.template
diff options
context:
space:
mode:
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>