From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- doc/stdlib/index-list.html.template | 95 +++++++++++++++++++++---------------- 1 file changed, 54 insertions(+), 41 deletions(-) (limited to 'doc/stdlib/index-list.html.template') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 833b5c4c..854c786c 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -3,7 +3,7 @@

Here is a short description of the Coq standard library, which is distributed with the system. -It provides a set of modules directly available +It provides a set of modules directly available through the Require Import command.

The standard library is composed of the following subdirectories:

@@ -12,27 +12,26 @@ through the Require Import command.

Init: The core library (automatically loaded when starting Coq)
-
+
theories/Init/Notations.v theories/Init/Datatypes.v theories/Init/Logic.v theories/Init/Logic_Type.v + theories/Init/Nat.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v theories/Init/Wf.v (theories/Init/Prelude.v)
- +
Logic: - Classical logic and dependent equality + Classical logic, dependent equality, extensionality, choice axioms
theories/Logic/SetIsType.v - theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.v - theories/Logic/Classical_Type.v (theories/Logic/Classical.v) theories/Logic/ClassicalFacts.v theories/Logic/Decidable.v @@ -57,8 +56,11 @@ through the Require Import command.

theories/Logic/IndefiniteDescription.v theories/Logic/FunctionalExtensionality.v theories/Logic/ExtensionalityFacts.v + theories/Logic/WeakFan.v + theories/Logic/WKL.v + theories/Logic/FinFun.v
- +
Structures: Algebraic structures (types with equality, with order, ...). DecidableType* and OrderedType* are there only for compatibility. @@ -83,7 +85,7 @@ through the Require Import command.

Bool: Booleans (basic functions and results)
-
+
theories/Bool/Bool.v theories/Bool/BoolEq.v theories/Bool/DecBool.v @@ -92,12 +94,12 @@ through the Require Import command.

theories/Bool/Zerob.v theories/Bool/Bvector.v
- +
Arith: Basic Peano arithmetic
-
- theories/Arith/Arith_base.v +
+ theories/Arith/PeanoNat.v theories/Arith/Le.v theories/Arith/Lt.v theories/Arith/Plus.v @@ -107,6 +109,7 @@ through the Require Import command.

theories/Arith/Between.v theories/Arith/Peano_dec.v theories/Arith/Compare_dec.v + (theories/Arith/Arith_base.v) (theories/Arith/Arith.v) theories/Arith/Min.v theories/Arith/Max.v @@ -173,8 +176,6 @@ through the Require Import command.

theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v - theories/ZArith/ZOdiv_def.v - theories/ZArith/ZOdiv.v theories/ZArith/Zdiv.v theories/ZArith/Zquot.v theories/ZArith/Zeuclid.v @@ -206,10 +207,13 @@ through the Require Import command.

theories/QArith/Qminmax.v
-
Numbers: +
Numbers: An experimental modular architecture for arithmetic
-
  Prelude: +
+
+
  Prelude: +
theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v @@ -219,6 +223,7 @@ through the Require Import command.

  NatInt: Abstract mixed natural/integer/cyclic arithmetic +
theories/Numbers/NatInt/NZAdd.v theories/Numbers/NatInt/NZAddOrder.v @@ -237,10 +242,10 @@ through the Require Import command.

theories/Numbers/NatInt/NZGcd.v theories/Numbers/NatInt/NZBits.v
- -
  Cyclic: +
  Cyclic: Abstract and 31-bits-based cyclic arithmetic +
theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -259,10 +264,10 @@ through the Require Import command.

theories/Numbers/Cyclic/Int31/Int31.v theories/Numbers/Cyclic/ZModulo/ZModulo.v
- -
  Natural: +
  Natural: Abstract and 31-bits-words-based natural arithmetic +
theories/Numbers/Natural/Abstract/NAdd.v theories/Numbers/Natural/Abstract/NAddOrder.v @@ -293,10 +298,11 @@ through the Require Import command.

theories/Numbers/Natural/BigN/NMake.v theories/Numbers/Natural/BigN/NMake_gen.v
- -
  Integer: - Abstract and concrete (especially 31-bits-words-based) integer arithmetic +
  Integer: + Abstract and concrete (especially 31-bits-words-based) integer + arithmetic +
theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -323,32 +329,32 @@ through the Require Import command.

theories/Numbers/Integer/BigZ/BigZ.v theories/Numbers/Integer/BigZ/ZMake.v
-
  Rational: Abstract and 31-bits-words-based rational arithmetic +
theories/Numbers/Rational/SpecViaQ/QSig.v theories/Numbers/Rational/BigQ/BigQ.v theories/Numbers/Rational/BigQ/QMake.v
- - - +
+
+
Relations: Relations (definitions and basic results)
-
+
theories/Relations/Relation_Definitions.v theories/Relations/Relation_Operators.v theories/Relations/Relations.v theories/Relations/Operators_Properties.v
- +
Sets: Sets (classical, constructive, finite, infinite, powerset, etc.)
-
+
theories/Sets/Classical_sets.v theories/Sets/Constructive_sets.v theories/Sets/Cpo.v @@ -372,32 +378,39 @@ through the Require Import command.

theories/Sets/Relations_3.v theories/Sets/Uniset.v
- +
Classes: -
+ +
theories/Classes/Init.v theories/Classes/RelationClasses.v theories/Classes/Morphisms.v theories/Classes/Morphisms_Prop.v theories/Classes/Morphisms_Relations.v theories/Classes/Equivalence.v + theories/Classes/CRelationClasses.v + theories/Classes/CMorphisms.v + theories/Classes/CEquivalence.v theories/Classes/EquivDec.v theories/Classes/SetoidTactics.v theories/Classes/SetoidClass.v theories/Classes/SetoidDec.v theories/Classes/RelationPairs.v + theories/Classes/DecidableClass.v
Setoids: -
+ +
theories/Setoids/Setoid.v
- +
Lists: Polymorphic lists, Streams (infinite sequences)
-
+
theories/Lists/List.v + theories/Lists/ListDec.v theories/Lists/ListSet.v theories/Lists/SetoidList.v theories/Lists/SetoidPermutation.v @@ -413,13 +426,14 @@ through the Require Import command.

theories/Vectors/Fin.v theories/Vectors/VectorDef.v theories/Vectors/VectorSpec.v + theories/Vectors/VectorEq.v (theories/Vectors/Vector.v)
Sorting: Axiomatizations of sorts
-
+
theories/Sorting/Heap.v theories/Sorting/Permutation.v theories/Sorting/Sorting.v @@ -432,7 +446,7 @@ through the Require Import command.

Wellfounded: Well-founded Relations
-
+
theories/Wellfounded/Disjoint_Union.v theories/Wellfounded/Inclusion.v theories/Wellfounded/Inverse_Image.v @@ -500,11 +514,11 @@ through the Require Import command.

theories/Strings/Ascii.v theories/Strings/String.v
- +
Reals: Formalization of real numbers
-
+
theories/Reals/Rdefinitions.v theories/Reals/Raxioms.v theories/Reals/RIneq.v @@ -566,14 +580,13 @@ through the Require Import command.

theories/Reals/SeqSeries.v theories/Reals/Sqrt_reg.v theories/Reals/Rlogic.v - theories/Reals/LegacyRfield.v (theories/Reals/Reals.v)
- +
Program: Support for dependently-typed programming.
-
+
theories/Program/Basics.v theories/Program/Wf.v theories/Program/Subset.v -- cgit v1.2.3