aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-01-13 17:21:21 +0000
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 12:14:16 +0100
commitf8cb1942284979bc7c325f2137fad1293380d855 (patch)
tree08e9e3ff7ac99c7c000bc4e0ca683a8e7eb677ea /doc/stdlib
parent7f207c26b603a40ecbb58377f6669935d0419366 (diff)
Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentation)
This commit r14895 comes apparently itself from commit r12010 in branch v8.2
Diffstat (limited to 'doc/stdlib')
-rw-r--r--doc/stdlib/index-list.html.template14
-rw-r--r--doc/stdlib/index-trailer.html2
2 files changed, 1 insertions, 15 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 75b5e7fea..9873dd071 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -1,17 +1,5 @@
-<!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>
-<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>
-
-<H1>The Coq Standard Library</H1>
+<h1>The Coq Standard Library</h1>
<p>Here is a short description of the Coq standard library, which is
distributed with the system.
diff --git a/doc/stdlib/index-trailer.html b/doc/stdlib/index-trailer.html
deleted file mode 100644
index 308b1d01b..000000000
--- a/doc/stdlib/index-trailer.html
+++ /dev/null
@@ -1,2 +0,0 @@
-</body>
-</html>