summaryrefslogtreecommitdiff
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.template15
1 files changed, 8 insertions, 7 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 5e95a692..0ab4e47b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -69,6 +69,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Logic/Description.v
theories/Logic/Epsilon.v
theories/Logic/IndefiniteDescription.v
+ theories/Logic/FunctionalExtensionality.v
</dd>
<dt> <b>Bool</b>:
@@ -256,12 +257,7 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
<dd>
theories/Numbers/Rational/BigQ/BigQ.v
- theories/Numbers/Rational/BigQ/Q0Make.v
- theories/Numbers/Rational/BigQ/QbiMake.v
- theories/Numbers/Rational/BigQ/QifMake.v
- theories/Numbers/Rational/BigQ/QMake_base.v
- theories/Numbers/Rational/BigQ/QpMake.v
- theories/Numbers/Rational/BigQ/QvMake.v
+ theories/Numbers/Rational/BigQ/QMake.v
theories/Numbers/Rational/SpecViaQ/QSig.v
</dd>
@@ -273,8 +269,10 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
theories/Relations/Relation_Operators.v
theories/Relations/Relations.v
theories/Relations/Operators_Properties.v
+<!-- Deprecated
theories/Relations/Rstar.v
theories/Relations/Newman.v
+-->
</dd>
<dt> <b>Sets</b>:
@@ -314,6 +312,7 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
theories/Classes/Morphisms_Relations.v
theories/Classes/Equivalence.v
theories/Classes/EquivDec.v
+ theories/Classes/Functions.v
theories/Classes/SetoidTactics.v
theories/Classes/SetoidClass.v
theories/Classes/SetoidDec.v
@@ -321,8 +320,11 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
</dd>
<dt> <b>Setoids</b>:
+
<dd>
theories/Setoids/Setoid.v
+ theories/Setoids/Setoid_tac.v
+ theories/Setoids/Setoid_Prop.v
</dd>
<dt> <b>Lists</b>:
@@ -477,7 +479,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
theories/Program/Utils.v
theories/Program/Syntax.v
theories/Program/Program.v
- theories/Program/FunctionalExtensionality.v
theories/Program/Combinators.v
</dd>