diff options
Diffstat (limited to 'doc/stdlib/index-list.html.template')
| -rw-r--r-- | doc/stdlib/index-list.html.template | 39 |
1 files changed, 15 insertions, 24 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7a24846b..7ee85fe8 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. @@ -210,7 +198,9 @@ through the <tt>Require Import</tt> command.</p> <dt> <b>Numbers</b>: An experimental modular architecture for arithmetic </dt> - <dt> <b> Prelude</b>: + <dd> + <dl> + <dt> <b> Prelude</b>:</dt> <dd> theories/Numbers/NumPrelude.v theories/Numbers/BigNumPrelude.v @@ -219,6 +209,7 @@ through the <tt>Require Import</tt> command.</p> <dt> <b> NatInt</b>: Abstract mixed natural/integer/cyclic arithmetic + </dt> <dd> theories/Numbers/NatInt/NZAdd.v theories/Numbers/NatInt/NZAddOrder.v @@ -231,10 +222,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/NatInt/NZDomain.v theories/Numbers/NatInt/NZProperties.v </dd> - </dt> - <dt> <b> Cyclic</b>: + <dt> <b> Cyclic</b>: Abstract and 31-bits-based cyclic arithmetic + </dt> <dd> theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -253,10 +244,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Cyclic/Int31/Int31.v theories/Numbers/Cyclic/ZModulo/ZModulo.v </dd> - </dt> - <dt> <b> Natural</b>: + <dt> <b> Natural</b>: Abstract and 31-bits-words-based natural arithmetic + </dt> <dd> theories/Numbers/Natural/Abstract/NAdd.v theories/Numbers/Natural/Abstract/NAddOrder.v @@ -279,10 +270,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/BigN/NMake.v theories/Numbers/Natural/BigN/NMake_gen.v </dd> - </dt> <dt> <b> Integer</b>: Abstract and concrete (especially 31-bits-words-based) integer arithmetic + </dt> <dd> theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -303,17 +294,17 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/BigZ/BigZ.v theories/Numbers/Integer/BigZ/ZMake.v </dd> - </dt> <dt><b> Rational</b>: Abstract and 31-bits-words-based rational arithmetic + </dt> <dd> theories/Numbers/Rational/SpecViaQ/QSig.v theories/Numbers/Rational/BigQ/BigQ.v theories/Numbers/Rational/BigQ/QMake.v </dd> - </dt> - </dt> + </dl> + </dd> <dt> <b>Relations</b>: Relations (definitions and basic results) @@ -353,7 +344,7 @@ through the <tt>Require Import</tt> command.</p> theories/Sets/Uniset.v </dd> - <dt> <b>Classes</b>: + <dt> <b>Classes</b>:</dt> <dd> theories/Classes/Init.v theories/Classes/RelationClasses.v @@ -368,7 +359,7 @@ through the <tt>Require Import</tt> command.</p> theories/Classes/RelationPairs.v </dd> - <dt> <b>Setoids</b>: + <dt> <b>Setoids</b>:</dt> <dd> theories/Setoids/Setoid.v </dd> |