<h1>The Rocq Standard Library</h1>

<p>This is the index of the Rocq standard library.
It provides a set of modules directly available
through the <tt>From Stdlib Require Import</tt> command.</p>

<!-- #include depends.svg -->

<p>The standard library is composed of the following subdirectories:</p>

<dl>
  <dt> <a name="logic"></a><b>Logic</b>:
    Logic, dependent equality, extensionality, choice axioms.
    Look at <a href="#classical-logic">classical-logic</a> for more elaborate results.
  </dt>
  <dd>
    theories/Logic/SetIsType.v
    theories/Logic/StrictProp.v
    theories/Logic/Decidable.v
    theories/Logic/Eqdep_dec.v
    theories/Logic/EqdepFacts.v
    theories/Logic/Eqdep.v
    theories/Logic/JMeq.v
    theories/Logic/RelationalChoice.v
    theories/Logic/Berardi.v
    theories/Logic/Hurkens.v
    theories/Logic/ProofIrrelevance.v
    theories/Logic/ProofIrrelevanceFacts.v
    theories/Logic/ConstructiveEpsilon.v
    theories/Logic/PropExtensionalityFacts.v
    theories/Logic/FunctionalExtensionality.v
    theories/Logic/ExtensionalFunctionRepresentative.v
    theories/Logic/ExtensionalityFacts.v
    theories/Logic/WeakFan.v
    theories/Logic/PropFacts.v
    theories/Logic/HLevels.v
    theories/Logic/Adjointification.v
  </dd>

  <dt> <a name="program"></a><b>Program</b>:
    Support for dependently-typed programming
    Beware that there are also Tactics.v and Wf.v files in Init.
  </dt>
  <dd>
    theories/Program/Subset.v
    theories/Program/Equality.v
    theories/Program/Syntax.v
    theories/Program/WfExtensionality.v
    theories/Program/Program.v
    theories/Program/Combinators.v
  </dd>

  <dt> <a name="relations"></a><b>Relations</b>:
    Relations (definitions and basic results)
  </dt>
  <dd>
    theories/Relations/Relation_Operators.v
    theories/Relations/Relations.v
    theories/Relations/Operators_Properties.v
  </dd>

  <dt> <a name="classes"></a><b>Classes</b>:
  </dt>
  <dd>
    theories/Classes/Morphisms_Relations.v
    theories/Classes/CEquivalence.v
    theories/Classes/SetoidClass.v
    theories/Classes/RelationPairs.v
    theories/Classes/DecidableClass.v
  </dd>

  <dt><a name="bool"></a><b>Bool</b>:
    Booleans (basic functions and results)
  </dt>
  <dd>
    theories/Bool/Bool.v
    theories/Bool/BoolEq.v
    theories/Bool/DecBool.v
    theories/Bool/IfProp.v
  </dd>

  <dt> <a name="structures"></a><b>Structures</b>:
    Basic "algebraic" structures: types with decidable equality and with order.
    Common instances can be found in <a href="#orders-ex">orders-ex</a>.
    More developped algebra can be found in the
    <a href="https://github.com/math-comp/math-comp">mathematical components
    library</a>.
  </dt>
  <dd>
    theories/Structures/Equalities.v
    theories/Structures/Orders.v
    theories/Structures/OrdersTac.v
    theories/Structures/OrdersFacts.v
    theories/Structures/GenericMinMax.v
  </dd>

  <dt> <a name="arith-base"></a><b>Arith-base</b>:
    Basic Peano Arithmetic.
    Everything can be loaded with From Stdlib Require Import Arith_base.
    To enjoy the ring and lia automatic tactic, you additionally need to load
    arith below, using From Stdlib Require Import Arith Lia.
  </dt>
  <dd>
    theories/Arith/PeanoNat.v
    theories/Arith/Between.v
    theories/Arith/Peano_dec.v
    theories/Arith/Compare_dec.v
    (theories/Arith/Arith_base.v)
    theories/Arith/Compare.v
    theories/Arith/EqNat.v
    theories/Arith/Euclid.v
    theories/Arith/Factorial.v
    theories/Arith/Wf_nat.v
    theories/Arith/Cantor.v
    theories/Arith/Zerob.v
    theories/Numbers/NumPrelude.v
    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/NZDiv.v
    theories/Numbers/NatInt/NZMulOrder.v
    theories/Numbers/NatInt/NZOrder.v
    theories/Numbers/NatInt/NZParity.v
    theories/Numbers/NatInt/NZPow.v
    theories/Numbers/NatInt/NZSqrt.v
    theories/Numbers/NatInt/NZLog.v
    theories/Numbers/NatInt/NZGcd.v
    theories/Numbers/NatInt/NZBits.v
    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/NMulOrder.v
    theories/Numbers/Natural/Abstract/NOrder.v
    theories/Numbers/Natural/Abstract/NStrongRec.v
    theories/Numbers/Natural/Abstract/NSub.v
    theories/Numbers/Natural/Abstract/NDiv.v
    theories/Numbers/Natural/Abstract/NDiv0.v
    theories/Numbers/Natural/Abstract/NMaxMin.v
    theories/Numbers/Natural/Abstract/NParity.v
    theories/Numbers/Natural/Abstract/NPow.v
    theories/Numbers/Natural/Abstract/NSqrt.v
    theories/Numbers/Natural/Abstract/NLog.v
    theories/Numbers/Natural/Abstract/NGcd.v
    theories/Numbers/Natural/Abstract/NLcm.v
    theories/Numbers/Natural/Abstract/NLcm0.v
    theories/Numbers/Natural/Abstract/NBits.v
    theories/Numbers/Natural/Abstract/NProperties.v
    theories/Classes/SetoidDec.v
  </dd>

  <dt> <a name="lists"></a><b>Lists</b>:
    Polymorphic lists
  </dt>
  <dd>
    theories/Lists/List.v
    theories/Lists/ListDec.v
    theories/Lists/ListSet.v
    theories/Lists/ListTactics.v
    theories/Numbers/NaryFunctions.v
    theories/Logic/WKL.v
    theories/Classes/EquivDec.v
  </dd>

  <dt> <a name="streams"></a><b>Streams</b>:
    Streams (infinite sequences)
  </dt>
  <dd>
    theories/Streams/Streams.v
    theories/Streams/StreamMemo.v
  </dd>

  <dt> <a name="positive"></a><b>PArith</b>:
    Binary representation of positive integers for effective computation.
    You may also want narith and zarith below for N and Z
    built on top of <a href="#positive">positive</a>.
  </dt>
  <dd>
    theories/Numbers/AltBinNotations.v
    theories/PArith/BinPosDef.v
    theories/PArith/BinPos.v
    theories/PArith/Pnat.v
    theories/PArith/POrderedType.v
    (theories/PArith/PArith.v)
  </dd>

  <dt> <a name="narith-base"></a><b>NArith-base</b>:
    Binary natural numbers.
    Everything can be loaded with From Stdlib Require Import NArith_base.
    To enjoy the ring automatic tactic, you need to load
    <a href="#narith">narith</a> below, using From Stdlib Require Import NArith.
  </dt>
  <dd>
    theories/NArith/BinNatDef.v
    theories/NArith/BinNat.v
    theories/NArith/Nnat.v
    theories/NArith/Ndec.v
    theories/NArith/Ndiv_def.v
    theories/NArith/Ngcd_def.v
    theories/NArith/Nsqrt_def.v
    (theories/NArith/NArith_base.v)
  </dd>

  <dt> <a name="narith"></a><b>NArith</b>:
    Binary natural numbers
  </dt>
  <dd>
    (theories/NArith/NArith.v)
  </dd>

  <dt> <a name="zarith-base"></a><b>ZArith-base</b>:
    Basic binary integers
  </dt>
  <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/ZLt.v
    theories/Numbers/Integer/Abstract/ZMul.v
    theories/Numbers/Integer/Abstract/ZMulOrder.v
    theories/Numbers/Integer/Abstract/ZSgnAbs.v
    theories/Numbers/Integer/Abstract/ZMaxMin.v
    theories/Numbers/Integer/Abstract/ZParity.v
    theories/Numbers/Integer/Abstract/ZPow.v
    theories/Numbers/Integer/Abstract/ZGcd.v
    theories/Numbers/Integer/Abstract/ZLcm.v
    theories/Numbers/Integer/Abstract/ZBits.v
    theories/Numbers/Integer/Abstract/ZProperties.v
    theories/Numbers/Integer/Abstract/ZDivFloor.v
    theories/Numbers/Integer/Abstract/ZDivTrunc.v
    theories/ZArith/BinIntDef.v
    theories/ZArith/BinInt.v
    theories/ZArith/Zorder.v
    theories/ZArith/Zcompare.v
    theories/ZArith/Znat.v
    theories/ZArith/Zmin.v
    theories/ZArith/Zmax.v
    theories/ZArith/Zminmax.v
    theories/ZArith/Zabs.v
    theories/ZArith/Zeven.v
    theories/ZArith/auxiliary.v
    theories/ZArith/ZArith_dec.v
    theories/ZArith/Zbool.v
    theories/ZArith/Zmisc.v
    theories/ZArith/Wf_Z.v
    theories/ZArith/Zhints.v
    (theories/ZArith/ZArith_base.v)
    theories/ZArith/Zpow_alt.v
    theories/ZArith/Int.v
  </dd>

  <dt> <a name="ring"></a><b>Ring</b>:
    Ring tactic.
  </dt>
  <dd>
    theories/ZArith/Zcomplements.v
    theories/ZArith/Zpow_def.v
    theories/ZArith/Zdiv.v
    theories/ZArith/Znumtheory.v
  </dd>

  <dt> <a name="arith"></a><b>Arith</b>:
    Basic Peano arithmetic
  </dt>
  <dd>
    (theories/Arith/Arith.v)
  </dd>

  <dt> <a name="zarith"></a><b>ZArith</b>:
    Binary encoding of integers.
    This binary encoding was initially developped to enable effective
    computations, compared to the unary encoding of nat. Proofs were then added
    making the types usable for mathematical proofs, although this was not
    the initial intent. If even-more efficient computations are needed, look
    at the <a href="#primitive-int">primitive-int</a> package below for 63 bits machine arithmetic
    or the coq-bignums package for arbitrary precision machine arithmetic.
    Everything can be imported with From Stdlib Require Import ZArith.
    Also contains the migromega tactic that can be loaded with
    From Stdlib Require Import Lia.
  </dt>
  <dd>
    theories/ZArith/Zpower.v
    theories/ZArith/Zquot.v
    (theories/ZArith/ZArith.v)
    theories/ZArith/Zgcd_alt.v
    theories/ZArith/Zwf.v
    theories/ZArith/Zpow_facts.v
    theories/ZArith/Zdiv_facts.v
    theories/ZArith/Zbitwise.v
    theories/Numbers/DecimalFacts.v
    theories/Numbers/DecimalNat.v
    theories/Numbers/DecimalPos.v
    theories/Numbers/DecimalN.v
    theories/Numbers/DecimalZ.v
    theories/Numbers/HexadecimalFacts.v
    theories/Numbers/HexadecimalNat.v
    theories/Numbers/HexadecimalPos.v
    theories/Numbers/HexadecimalN.v
    theories/Numbers/HexadecimalZ.v
  </dd>

  <dt> <a name="unicode"></a><b>Unicode</b>:
    Unicode-based alternative notations
  </dt>
  <dd>
    theories/Unicode/Utf8_core.v
    theories/Unicode/Utf8.v
  </dd>

  <dt> <a name="primitive-int"></a><b>Primitive Integers</b>:
    Interface for hardware integers (63 rather than 64 bits due to OCaml
    garbage collector). This enables very efficient arithmetic, for developing
    tactics for proofs by reflection for instance.
  </dt>
  <dd>
    theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
    theories/Numbers/Cyclic/Abstract/NZCyclic.v
    theories/Numbers/Cyclic/Abstract/DoubleType.v
    theories/Numbers/Cyclic/Int63/Cyclic63.v
    theories/Numbers/Cyclic/Int63/Uint63.v
    theories/Numbers/Cyclic/Int63/Sint63.v
    theories/Numbers/Cyclic/Int63/Ring63.v
  </dd>

  <dt> <a name="primitive-floats"></a><b>Floats</b>:
    Efficient machine floating-point arithmetic
    Interface to hardware floating-point arithmetic for efficient computations.
    This offers a basic model of floating-point arithmetic but is not very
    usable alone. Look at the coq-flocq package for an actual model of
    floating-point arithmetic, including links to Stdlib <a href="#reals">reals</a> and the current
    Floats.
  </dt>
  <dd>
    theories/Floats/FloatLemmas.v
    (theories/Floats/Floats.v)
  </dd>

  <dt> <a name="primitive-array"></a><b>Primitive Arrays</b>:
    Persistent native arrays, enabling efficient computations with arrays.
  </dt>
  <dd>
    theories/Array/PArray.v
  </dd>

  <dt> <a name="vectors"></a><b>Vectors</b>:
    Dependent datastructures storing their length.
    This is known to be technically difficult to use. It is often much better
    to use a dependent pair with a list and a proof about its length,
    as provided by the tuple type in package coq-mathcomp-ssreflect,
    allowing almost transparent mixing with lists.
  </dt>
  <dd>
    theories/Vectors/Fin.v
    theories/Vectors/VectorDef.v
    theories/Vectors/VectorSpec.v
    theories/Vectors/VectorEq.v
    (theories/Vectors/Vector.v)
    theories/Vectors/FinFun.v
    theories/Vectors/Bvector.v
  </dd>

  <dt> <a name="strings"></a><b>Strings</b>
    Implementation of string as list of ASCII characters
    Beware that there is also a Byte.v file in Init.
  </dt>
  <dd>
    theories/Strings/Byte.v
    theories/Strings/Ascii.v
    theories/Strings/String.v
    theories/Strings/BinaryString.v
    theories/Strings/HexString.v
    theories/Strings/OctalString.v
    theories/Numbers/DecimalString.v
    theories/Numbers/HexadecimalString.v
  </dd>

  <dt> <a name="classical-logic"></a><b>Classical Logic</b>:
    Classical logic, dependent equality, extensionality, choice axioms
  </dt>
  <dd>
    theories/Logic/Classical_Pred_Type.v
    theories/Logic/Classical_Prop.v
    (theories/Logic/Classical.v)
    theories/Logic/ClassicalFacts.v
    theories/Logic/ChoiceFacts.v
    theories/Logic/ClassicalChoice.v
    theories/Logic/ClassicalDescription.v
    theories/Logic/ClassicalEpsilon.v
    theories/Logic/ClassicalUniqueChoice.v
    theories/Logic/SetoidChoice.v
    theories/Logic/Diaconescu.v
    theories/Logic/Description.v
    theories/Logic/Epsilon.v
    theories/Logic/IndefiniteDescription.v
    theories/Logic/PropExtensionality.v
  </dd>

  <dt> <a name="sets"></a><b>Sets</b>:
    Classical sets. This is known to be outdated. More modern alternatives
    can be found in coq-mathcomp-ssreflect (for finite sets)
    and coq-mathcomp-classical (for classical sets) or coq-stdpp.
  </dt>
  <dd>
    theories/Sets/Classical_sets.v
    theories/Sets/Constructive_sets.v
    theories/Sets/Cpo.v
    theories/Sets/Ensembles.v
    theories/Sets/Finite_sets_facts.v
    theories/Sets/Finite_sets.v
    theories/Sets/Image.v
    theories/Sets/Infinite_sets.v
    theories/Sets/Integers.v
    theories/Sets/Multiset.v
    theories/Sets/Partial_Order.v
    theories/Sets/Permut.v
    theories/Sets/Powerset_Classical_facts.v
    theories/Sets/Powerset_facts.v
    theories/Sets/Powerset.v
    theories/Sets/Relations_1_facts.v
    theories/Sets/Relations_1.v
    theories/Sets/Relations_2_facts.v
    theories/Sets/Relations_2.v
    theories/Sets/Relations_3_facts.v
    theories/Sets/Relations_3.v
    theories/Sets/Uniset.v
  </dd>

  <dt> <a name="sorting"></a><b>Sorting</b>:
    Axiomatizations of sorts
  </dt>
  <dd>
    theories/Sorting/SetoidList.v
    theories/Sorting/SetoidPermutation.v
    theories/Sorting/Heap.v
    theories/Sorting/Permutation.v
    theories/Sorting/Sorting.v
    theories/Sorting/PermutEq.v
    theories/Sorting/PermutSetoid.v
    theories/Sorting/Mergesort.v
    theories/Sorting/Sorted.v
    theories/Sorting/CPermutation.v
  </dd>

  <dt> <a name="orders-ex"></a><b>Structure Instances</b>:
    Instances of order structures from <a href="#structures">Structures</a> above.
    DecidableType* and OrderedType* are there only for compatibility.
  </dt>
  <dd>
    theories/Structures/EqualitiesFacts.v
    theories/Structures/OrdersAlt.v
    theories/Structures/OrdersEx.v
    theories/Structures/OrdersLists.v
    theories/Structures/DecidableType.v
    theories/Structures/DecidableTypeEx.v
    theories/Structures/OrderedType.v
    theories/Structures/OrderedTypeAlt.v
    theories/Structures/OrderedTypeEx.v
    theories/Structures/BoolOrder.v
  </dd>

  <dt> <a name="primitive-string"></a><b>Primitive Strings</b>
    Native string type
  </dt>
  <dd>
    theories/Strings/PString.v
  </dd>

  <dt> <a name="qarith-base"></a><b>QArith-base</b>:
    Basic binary rational numbers.
    Look at <a href="#qarith">qarith</a> below for more functionalities with the field
    and Lqa tactics.
  </dt>
  <dd>
    theories/QArith/QArith_base.v
    theories/QArith/Qreduction.v
    theories/QArith/QOrderedType.v
    theories/QArith/Qminmax.v
  </dd>

  <dt> <a name="field"></a><b>Field</b>:
    Field tactic.
  </dt>
  <dd>
    theories/QArith/Qpower.v
    theories/QArith/Qring.v
    theories/QArith/Qfield.v
    theories/QArith/Qcanon.v
    theories/QArith/Qround.v
  </dd>

  <dt> <a name="qarith"></a><b>QArith</b>:
    Binary rational numbers, made on top of <a href="#zarith">zarith</a>.
    Those enable effective computations in arbitrary precision exact rational
    arithmetic. Those rationals are known to be difficult to use for
    mathematical proofs because there is no canonical representation
    (2/3 and 4/6 are not equal for instance). For even more efficient
    computation, look at the coq-bignums package which uses machine integers.
    For mathematical proofs, the rat type of the coq-mathcomp-algebra package
    are much more comfortable, although they don't enjoy efficient computation
    (coq-coqeal offers a refinement with coq-bignums that enables to enjoy
    both aspects).
  </dt>
  <dd>
    theories/QArith/Qabs.v
    (theories/QArith/QArith.v)
    theories/QArith/Qcabs.v
    theories/Numbers/DecimalQ.v
    theories/Numbers/HexadecimalQ.v
  </dd>

  <dt> <a name="reals"></a><b>Reals</b>:
    Formalization of real numbers.
    Most of it can be loaded with From Stdlib Require Import Reals.
    Also contains the micromega tactics, loadable with
    From Stdlib Require Import Lra. and From Stdlib Require Import Psatz.
  </dt>
  <dd>
    <dl>
  <dt> <b>Classical Reals</b>:
    Real numbers with excluded middle, total order and least upper bounds
  </dt>
  <dd>
    theories/Reals/Rdefinitions.v
    theories/Reals/ClassicalDedekindReals.v
    theories/Reals/ClassicalConstructiveReals.v
    theories/Reals/Raxioms.v
    theories/Reals/RIneq.v
    theories/Reals/DiscrR.v
    theories/Reals/ROrderedType.v
    theories/Reals/Rminmax.v
    (theories/Reals/Rbase.v)
    theories/Reals/RList.v
    theories/Reals/Ranalysis.v
    theories/Reals/Rbasic_fun.v
    theories/Reals/Rderiv.v
    theories/Reals/Rfunctions.v
    theories/Reals/Zfloor.v
    theories/Reals/Rgeom.v
    theories/Reals/R_Ifp.v
    theories/Reals/Rlimit.v
    theories/Reals/Rseries.v
    theories/Reals/Rsigma.v
    theories/Reals/R_sqr.v
    theories/Reals/Rtrigo_fun.v
    theories/Reals/Rtrigo1.v
    theories/Reals/Rtrigo.v
    theories/Reals/Rtrigo_facts.v
    theories/Reals/Ratan.v
    theories/Reals/Machin.v
    theories/Reals/SplitAbsolu.v
    theories/Reals/SplitRmult.v
    theories/Reals/Alembert.v
    theories/Reals/AltSeries.v
    theories/Reals/ArithProp.v
    theories/Reals/Binomial.v
    theories/Reals/Cauchy_prod.v
    theories/Reals/Cos_plus.v
    theories/Reals/Cos_rel.v
    theories/Reals/Exp_prop.v
    theories/Reals/Integration.v
    theories/Reals/MVT.v
    theories/Reals/NewtonInt.v
    theories/Reals/PSeries_reg.v
    theories/Reals/PartSum.v
    theories/Reals/R_sqrt.v
    theories/Reals/Ranalysis1.v
    theories/Reals/Ranalysis2.v
    theories/Reals/Ranalysis3.v
    theories/Reals/Ranalysis4.v
    theories/Reals/Ranalysis5.v
    theories/Reals/Ranalysis_reg.v
    theories/Reals/Rcomplete.v
    theories/Reals/RiemannInt.v
    theories/Reals/RiemannInt_SF.v
    theories/Reals/Rpow_def.v
    theories/Reals/Rpower.v
    theories/Reals/Rprod.v
    theories/Reals/Rsqrt_def.v
    theories/Reals/Rtopology.v
    theories/Reals/Rtrigo_alt.v
    theories/Reals/Rtrigo_calc.v
    theories/Reals/Rtrigo_def.v
    theories/Reals/Rtrigo_reg.v
    theories/Reals/SeqProp.v
    theories/Reals/SeqSeries.v
    theories/Reals/Sqrt_reg.v
    theories/Reals/Rlogic.v
    theories/Reals/Rregisternames.v
    (theories/Reals/Reals.v)
    theories/Reals/Runcountable.v
  </dd>
  <dt> <b>Abstract Constructive Reals</b>:
    Interface of constructive reals, proof of equivalence of all implementations. EXPERIMENTAL 
  </dt>
  <dd>
    theories/Reals/Abstract/ConstructiveReals.v
    theories/Reals/Abstract/ConstructiveRealsMorphisms.v
    theories/Reals/Abstract/ConstructiveLUB.v
    theories/Reals/Abstract/ConstructiveAbs.v
    theories/Reals/Abstract/ConstructiveLimits.v
    theories/Reals/Abstract/ConstructiveMinMax.v
    theories/Reals/Abstract/ConstructivePower.v
    theories/Reals/Abstract/ConstructiveSum.v
  </dd>
  <dt> <b>Constructive Cauchy Reals</b>:
    Cauchy sequences of rational numbers, implementation of the interface. EXPERIMENTAL
  </dt>
  <dd>
    theories/Reals/Cauchy/ConstructiveRcomplete.v
    theories/Reals/Cauchy/ConstructiveCauchyReals.v
    theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
    theories/Reals/Cauchy/ConstructiveCauchyAbs.v
    theories/Reals/Qreals.v
    theories/Numbers/DecimalR.v
    theories/Numbers/HexadecimalR.v
  </dd>

  </dl>
  </dd>

  <dt> <a name="fmaps-fsets-msets"></a><b>MSets</b>:
    Modular implementation of finite sets using lists or
    efficient trees. This is a modernization of FSets.
  </dt>
  <dd>
    theories/MSets/MSetInterface.v
    theories/MSets/MSetFacts.v
    theories/MSets/MSetDecide.v
    theories/MSets/MSetProperties.v
    theories/MSets/MSetEqProperties.v
    theories/MSets/MSetWeakList.v
    theories/MSets/MSetList.v
    theories/MSets/MSetGenTree.v
    theories/MSets/MSetAVL.v
    theories/MSets/MSetRBT.v
    theories/MSets/MSetPositive.v
    theories/MSets/MSetToFiniteSet.v
    (theories/MSets/MSets.v)
  </dd>

  <dt> <b>FSets</b>:
    Modular implementation of finite sets/maps using lists or
    efficient trees. For sets, please consider the more
    modern MSets.
  </dt>
  <dd>
    theories/FSets/FSetInterface.v
    theories/FSets/FSetBridge.v
    theories/FSets/FSetFacts.v
    theories/FSets/FSetDecide.v
    theories/FSets/FSetProperties.v
    theories/FSets/FSetEqProperties.v
    theories/FSets/FSetList.v
    theories/FSets/FSetWeakList.v
    theories/FSets/FSetCompat.v
    theories/FSets/FSetAVL.v
    theories/FSets/FSetPositive.v
    (theories/FSets/FSets.v)
    theories/FSets/FSetToFiniteSet.v
    theories/FSets/FMapInterface.v
    theories/FSets/FMapWeakList.v
    theories/FSets/FMapList.v
    theories/FSets/FMapPositive.v
    theories/FSets/FMapFacts.v
    (theories/FSets/FMaps.v)
    theories/FSets/FMapAVL.v
    theories/FSets/FMapFullAVL.v
  </dd>

  <dt> <a name="wellfounded"></a><b>Wellfounded</b>:
    Well-founded Relations
  </dt>
  <dd>
    theories/Wellfounded/Disjoint_Union.v
    theories/Wellfounded/Inclusion.v
    theories/Wellfounded/Inverse_Image.v
    theories/Wellfounded/Lexicographic_Exponentiation.v
    theories/Wellfounded/Lexicographic_Product.v
    theories/Wellfounded/List_Extension.v
    theories/Wellfounded/Transitive_Closure.v
    theories/Wellfounded/Union.v
    theories/Wellfounded/Wellfounded.v
    theories/Wellfounded/Well_Ordering.v
  </dd>

  <dt> <a name="compat"></a><b>Compat</b>:
    Compatibility wrappers for previous versions of Stdlib
  </dt>
  <dd>
    theories/Compat/AdmitAxiom.v
    theories/Compat/Stdlib818.v
  </dd>

  <dt> <a name="all"></a><b>All</b>:
    Require the whole Stdlib
  </dt>
  <dd>
    (theories/All/All.v)
  </dd>
</dl>