From 8a2c029b0ae88888efe707c00f1a288e5c17cfb3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 19 Jan 2009 11:05:02 +0000
Subject: - Structuring Numbers and fixing Setoid in stdlib's doc. - Adding
 ability to use "_" in syntax for binders (as in "exists _:nat, True").

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-syn.tex           |   2 +-
 doc/stdlib/index-list.html.template | 165 ++++++++++++++++++++----------------
 2 files changed, 91 insertions(+), 76 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 6ade546b07..77eb292851 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -36,7 +36,7 @@ string \verb="A /\ B"= (called a {\em notation}) tells how it is
 symbolically written.
 
 A notation is always surrounded by double quotes (excepted when the
-abbreviation is a single ident, see \ref{Abbreviations}). The
+abbreviation is a single identifier, see \ref{Abbreviations}). The
 notation is composed of {\em tokens} separated by spaces.  Identifiers
 in the string (such as \texttt{A} and \texttt{B}) are the {\em
 parameters} of the notation. They must occur at least once each in the
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 64bf252f28..6b35dfa992 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -180,86 +180,103 @@ through the <tt>Require Import</tt> command.</p>
   </dd>
 
   <dt> <b>Numbers</b>: 
-    A modular axiomatic construction for numbers
+    An experimental modular architecture for arithmetic
   </dt>
-  <dd>
-  theories/Numbers/NumPrelude.v
-  theories/Numbers/BigNumPrelude.v
-  theories/Numbers/NaryFunctions.v
-  </dd>
-  
-  <dd>
-theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
-theories/Numbers/Cyclic/Abstract/NZCyclic.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
-theories/Numbers/Cyclic/Int31/Cyclic31.v
-theories/Numbers/Cyclic/Int31/Int31.v
-theories/Numbers/Cyclic/ZModulo/ZModulo.v
-  </dd>
+    <dt> <b>&nbsp;&nbsp;Prelude</b>: 
+    <dd>
+    theories/Numbers/NumPrelude.v
+    theories/Numbers/BigNumPrelude.v
+    theories/Numbers/NaryFunctions.v
+    </dd>
 
-  <dd>
-    theories/Numbers/Integer/Abstract/ZAdd.v
-theories/Numbers/Integer/Abstract/ZAddOrder.v
-theories/Numbers/Integer/Abstract/ZAxioms.v
-theories/Numbers/Integer/Abstract/ZBase.v
-theories/Numbers/Integer/Abstract/ZDomain.v
-theories/Numbers/Integer/Abstract/ZLt.v
-theories/Numbers/Integer/Abstract/ZMul.v
-theories/Numbers/Integer/Abstract/ZMulOrder.v
-theories/Numbers/Integer/BigZ/BigZ.v
-theories/Numbers/Integer/BigZ/ZMake.v
-theories/Numbers/Integer/Binary/ZBinary.v
-theories/Numbers/Integer/NatPairs/ZNatPairs.v
-theories/Numbers/Integer/SpecViaZ/ZSig.v
-theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
-  </dd>
+    <dt> <b>&nbsp;&nbsp;NatInt</b>:
+       Abstract mixed natural/integer/cyclic arithmetic
+    <dd>
+    theories/Numbers/NatInt/NZAdd.v
+    theories/Numbers/NatInt/NZAddOrder.v
+    theories/Numbers/NatInt/NZAxioms.v
+    theories/Numbers/NatInt/NZBase.v
+    theories/Numbers/NatInt/NZMul.v
+    theories/Numbers/NatInt/NZMulOrder.v
+    theories/Numbers/NatInt/NZOrder.v
+    </dd>
+    </dt>
 
-  <dd>
-theories/Numbers/NatInt/NZAdd.v
-theories/Numbers/NatInt/NZAddOrder.v
-theories/Numbers/NatInt/NZAxioms.v
-theories/Numbers/NatInt/NZBase.v
-theories/Numbers/NatInt/NZMul.v
-theories/Numbers/NatInt/NZMulOrder.v
-theories/Numbers/NatInt/NZOrder.v
-  </dd>
+    <dt> <b>&nbsp;&nbsp;Cyclic</b>: 
+       Abstract and 31-bits-based cyclic arithmetic
+    <dd>
+    theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+    theories/Numbers/Cyclic/Abstract/NZCyclic.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+    theories/Numbers/Cyclic/Int31/Cyclic31.v
+    theories/Numbers/Cyclic/Int31/Int31.v
+    theories/Numbers/Cyclic/ZModulo/ZModulo.v
+    </dd>
+    </dt>
 
-  <dd>
-theories/Numbers/Natural/Abstract/NAdd.v
-theories/Numbers/Natural/Abstract/NAddOrder.v
-theories/Numbers/Natural/Abstract/NAxioms.v
-theories/Numbers/Natural/Abstract/NBase.v
-theories/Numbers/Natural/Abstract/NDefOps.v
-theories/Numbers/Natural/Abstract/NIso.v
-theories/Numbers/Natural/Abstract/NMul.v
-theories/Numbers/Natural/Abstract/NMulOrder.v
-theories/Numbers/Natural/Abstract/NOrder.v
-theories/Numbers/Natural/Abstract/NStrongRec.v
-theories/Numbers/Natural/Abstract/NSub.v
-theories/Numbers/Natural/BigN/BigN.v
-theories/Numbers/Natural/BigN/Nbasic.v
-theories/Numbers/Natural/BigN/NMake.v
-theories/Numbers/Natural/Binary/NBinary.v
-theories/Numbers/Natural/Binary/NBinDefs.v
-theories/Numbers/Natural/Peano/NPeano.v
-theories/Numbers/Natural/SpecViaZ/NSig.v
-theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
-  </dd>
+    <dt> <b>&nbsp;&nbsp;Natural</b>: 
+       Abstract and 31-bits-words-based natural arithmetic
+    <dd>
+    theories/Numbers/Natural/Abstract/NAdd.v
+    theories/Numbers/Natural/Abstract/NAddOrder.v
+    theories/Numbers/Natural/Abstract/NAxioms.v
+    theories/Numbers/Natural/Abstract/NBase.v
+    theories/Numbers/Natural/Abstract/NDefOps.v
+    theories/Numbers/Natural/Abstract/NIso.v
+    theories/Numbers/Natural/Abstract/NMul.v
+    theories/Numbers/Natural/Abstract/NMulOrder.v
+    theories/Numbers/Natural/Abstract/NOrder.v
+    theories/Numbers/Natural/Abstract/NStrongRec.v
+    theories/Numbers/Natural/Abstract/NSub.v
+    theories/Numbers/Natural/Binary/NBinary.v
+    theories/Numbers/Natural/Binary/NBinDefs.v
+    theories/Numbers/Natural/Peano/NPeano.v
+    theories/Numbers/Natural/SpecViaZ/NSig.v
+    theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+    theories/Numbers/Natural/BigN/BigN.v
+    theories/Numbers/Natural/BigN/Nbasic.v
+    theories/Numbers/Natural/BigN/NMake.v
+    </dd>
+    </dt>
 
-  <dd>
+    <dt> <b>&nbsp;&nbsp;Integer</b>: 
+       Abstract and concrete (especially 31-bits-words-based) integer arithmetic
+    <dd>
+    theories/Numbers/Integer/Abstract/ZAdd.v
+    theories/Numbers/Integer/Abstract/ZAddOrder.v
+    theories/Numbers/Integer/Abstract/ZAxioms.v
+    theories/Numbers/Integer/Abstract/ZBase.v
+    theories/Numbers/Integer/Abstract/ZDomain.v
+    theories/Numbers/Integer/Abstract/ZLt.v
+    theories/Numbers/Integer/Abstract/ZMul.v
+    theories/Numbers/Integer/Abstract/ZMulOrder.v
+    theories/Numbers/Integer/Binary/ZBinary.v
+    theories/Numbers/Integer/NatPairs/ZNatPairs.v
+    theories/Numbers/Integer/SpecViaZ/ZSig.v
+    theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+    theories/Numbers/Integer/BigZ/BigZ.v
+    theories/Numbers/Integer/BigZ/ZMake.v
+    </dd>
+    </dt>
+
+    <dt><b>&nbsp;&nbsp;Rational</b>:
+       Abstract and 31-bits-words-based rational arithmetic
+    <dd>
+    theories/Numbers/Rational/SpecViaQ/QSig.v
     theories/Numbers/Rational/BigQ/BigQ.v
     theories/Numbers/Rational/BigQ/QMake.v
-    theories/Numbers/Rational/SpecViaQ/QSig.v
-  </dd>
+    </dd>
+    </dt>
+  </dt>
   
   <dt> <b>Relations</b>:
        Relations (definitions and basic results)
@@ -318,8 +335,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
   <dt> <b>Setoids</b>:
   <dd> 
     theories/Setoids/Setoid.v
-    theories/Setoids/Setoid_Prop.v
-    theories/Setoids/Setoid_tac.v
   </dd>
     
   <dt> <b>Lists</b>:
-- 
cgit v1.2.3