diff options
Diffstat (limited to 'doc/stdlib/index-list.html.template')
| -rw-r--r-- | doc/stdlib/index-list.html.template | 46 |
1 files changed, 14 insertions, 32 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 9216c81f..8c09b23a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -18,6 +18,7 @@ through the <tt>Require Import</tt> command.</p> theories/Init/Logic.v theories/Init/Logic_Type.v theories/Init/Nat.v + theories/Init/Decimal.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v @@ -46,6 +47,7 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/ClassicalDescription.v theories/Logic/ClassicalEpsilon.v theories/Logic/ClassicalUniqueChoice.v + theories/Logic/SetoidChoice.v theories/Logic/Berardi.v theories/Logic/Diaconescu.v theories/Logic/Hurkens.v @@ -55,7 +57,10 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/Description.v theories/Logic/Epsilon.v theories/Logic/IndefiniteDescription.v + theories/Logic/PropExtensionality.v + theories/Logic/PropExtensionalityFacts.v theories/Logic/FunctionalExtensionality.v + theories/Logic/ExtensionalFunctionRepresentative.v theories/Logic/ExtensionalityFacts.v theories/Logic/WeakFan.v theories/Logic/WKL.v @@ -220,8 +225,13 @@ through the <tt>Require Import</tt> command.</p> <dd> theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v - theories/Numbers/BigNumPrelude.v theories/Numbers/NaryFunctions.v + theories/Numbers/DecimalFacts.v + theories/Numbers/DecimalNat.v + theories/Numbers/DecimalPos.v + theories/Numbers/DecimalN.v + theories/Numbers/DecimalZ.v + theories/Numbers/DecimalString.v </dd> <dt> <b> NatInt</b>: @@ -252,16 +262,7 @@ through the <tt>Require Import</tt> command.</p> <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/Abstract/DoubleType.v theories/Numbers/Cyclic/Int31/Cyclic31.v theories/Numbers/Cyclic/Int31/Ring31.v theories/Numbers/Cyclic/Int31/Int31.v @@ -294,12 +295,6 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Binary/NBinary.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 - theories/Numbers/Natural/BigN/NMake_gen.v </dd> <dt> <b> Integer</b>: @@ -327,19 +322,6 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/Abstract/ZDivTrunc.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><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> </dl> </dd> @@ -614,8 +596,8 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Compat/AdmitAxiom.v - theories/Compat/Coq84.v - theories/Compat/Coq85.v theories/Compat/Coq86.v + theories/Compat/Coq87.v + theories/Compat/Coq88.v </dd> </dl> |