summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /doc
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'doc')
-rw-r--r--doc/Makefile4
-rw-r--r--doc/stdlib/index-list.html.template15
2 files changed, 14 insertions, 5 deletions
diff --git a/doc/Makefile b/doc/Makefile
index 6209b0c8..403e2047 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -116,7 +116,7 @@ REFMANCOQTEXFILES=\
refman/Setoid.v.tex refman/Helm.tex # refman/Natural.v.tex
REFMANTEXFILES=\
- refman/headers.tex \
+ refman/headers.sty \
refman/Reference-Manual.tex refman/RefMan-pre.tex \
refman/RefMan-int.tex refman/RefMan-pro.tex \
refman/RefMan-com.tex \
@@ -152,7 +152,7 @@ refman/Reference-Manual.pdf: refman/Reference-Manual.tex
### Reference Manual (browsable format)
-refman/Reference-Manual.html: refman/Reference-Manual.dvi # to ensure bbl file
+refman/Reference-Manual.html: refman/headers.hva refman/Reference-Manual.dvi # to ensure bbl file
(cd refman; hevea -fix -exec xxdate.exe ./Reference-Manual.tex)
refman/html/index.html: refman/Reference-Manual.html $(REFMANPNGFILES) \
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index f63b6cf4..81ab034b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -1,8 +1,13 @@
-<html>
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+
+<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
-<link rel="stylesheet" href="coqdoc.css" type="text/css">
-<title>The Coq Standard Library
+<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
+<link rel="stylesheet" href="css/context.css" type="text/css">
+<title>The Coq Standard Library</title>
</head>
<body>
@@ -60,6 +65,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Logic/Hurkens.v
theories/Logic/ProofIrrelevance.v
theories/Logic/ProofIrrelevanceFacts.v
+ theories/Logic/ConstructiveEpsilon.v
</dd>
<dt> <b>Arith</b>:
@@ -203,6 +209,8 @@ through the <tt>Require Import</tt> command.</p>
theories/Reals/SeqProp.v
theories/Reals/SeqSeries.v
theories/Reals/Sqrt_reg.v
+ theories/Reals/LegacyRfield.v
+ theories/Reals/Rpow_def.v
(theories/Reals/Reals.v)
</dd>
@@ -289,6 +297,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Lists/SetoidList.v
theories/Lists/Streams.v
theories/Lists/TheoryList.v
+ theories/Lists/ListTactics.v
</dd>
<dt> <b>FSets</b>: