aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-29 16:58:51 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-29 16:58:51 +0000
commitf34f0420899594847b6e7633a4488f034a4300f6 (patch)
tree1c089994f27280b35a181e8bb69ae87878150359 /doc/stdlib
parent1903011fd6faf22cde837cbdd140306ea20e4a99 (diff)
Produce better html code with coqdoc and improve doc:
- correct nesting of a and div (fixes bug #2022) - use span instead of div for inline parts - fix standard lib template missing/new links - use -g to produce the stdlib doc (no proofs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11724 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/index-list.html.template5
1 files changed, 1 insertions, 4 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 86dd5df22..84e4e4fa0 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>:
@@ -268,8 +269,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
theories/Relations/Relation_Operators.v
theories/Relations/Relations.v
theories/Relations/Operators_Properties.v
- theories/Relations/Rstar.v
- theories/Relations/Newman.v
</dd>
<dt> <b>Sets</b>:
@@ -313,7 +312,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
theories/Classes/SetoidClass.v
theories/Classes/SetoidDec.v
theories/Classes/SetoidAxioms.v
- theories/Classes/Functions.v
</dd>
<dt> <b>Setoids</b>:
@@ -475,7 +473,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>