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