\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Recent changes

Unreleased changes

Changed 

in MSets, Numbers, Structures
- several module types were turned into plain modules to accomodate for rocq-prover/rocq#22580. The major difference is that they cannot be used as sealing adscriptions anymore. In order to ease the transition, corresponding module types were added alongside with the standard naming scheme Module Foo ↦ Module Type FooT (#318, by Pierre-Marie Pédrot).

Version 9.2

Changes in 9.2.0

Changed 

in RelationPairs.v
- changed notations _ @@1 and _ @@2 from level 30 to level 1 (#235, by Pierre Roux).
in FMapAVL.v
- changed notations _ #1, _ #2, _ #l, _ #o and _ #r from level 9 to level 1 (#235, by Pierre Roux).
- changed notation << _ , _ , _ >> from level 9 to level 0 (#235, by Pierre Roux).
in MSetAVL.v
- changed notations _ #1, _ #2, _ #l, _ #b and _ #r from level 9 to level 1 (#235, by Pierre Roux).
- changed notation << _ , _ , _ >> from level 9 to level 0 (#235, by Pierre Roux).
in ZNatPairs.v
- changed notations _ #1 and _ #2 from level 9 to level 1 (#235, by Pierre Roux).
in NZBits.v
- changed notation _ .[ _ ] from level 5 to level 1 (#235, by Pierre Roux).
in NZDomain.v
- changed notation [ _ ] from level 7 to level 0 (#235, by Pierre Roux).
in theories/Zmod/Bits.v
- Fixed lemma bits.skipn_app to actually describe the interaction between the titular functions. Developments relying on the previous tautological statement can restore it by adding that version of the lemma to the codebase (#258, by Andres Erbsen).

Version 9.1

Changes in 9.1.0

Changed 

in RelationPairs.v
- changed notations _ @@1 and _ @@2 from level 30 to level 1 (#235, by Pierre Roux).
in FMapAVL.v
- changed notations _ #1, _ #2, _ #l, _ #o and _ #r from level 9 to level 1 (#235, by Pierre Roux).
- changed notation << _ , _ , _ >> from level 9 to level 0 (#235, by Pierre Roux).
in MSetAVL.v
- changed notations _ #1, _ #2, _ #l, _ #b and _ #r from level 9 to level 1 (#235, by Pierre Roux).
- changed notation << _ , _ , _ >> from level 9 to level 0 (#235, by Pierre Roux).
in ZNatPairs.v
- changed notations _ #1 and _ #2 from level 9 to level 1 (#235, by Pierre Roux).
in NZBits.v
- changed notation _ .[ _ ] from level 5 to level 1 (#235, by Pierre Roux).
in NZDomain.v
- changed notation [ _ ] from level 7 to level 0 (#235, by Pierre Roux).
in theories/Zmod/Bits.v
- Fixed lemma bits.skipn_app to actually describe the interaction between the titular functions. Developments relying on the previous tautological statement can resore it by adding that version of the lemma to the codebase (#258, by Andres Erbsen).

Changed 

Internal dependencies between about 50 stdlib files
- To diagnose a failing qualified reference use From Stdlib Require All. Locate My.Qualified.reference. Then add a Require command for the appropriately granular containing file (#150, by Andres Erbsen).
in FinFun
- Split out non-Fin-specific definitons into Lists.Finite (#154, by Andres Erbsen).
in HLevels.v
- Split into HLevels into HLevelsBase, which does not depend on axioms, and HLevels, which exports the former and provides the previous functionality (#133, by Andres Erbsen).
in NsatzTactic.v
- Split NsatzTactic into a smaller NsatzTactic that only depends on setoid_ring, and per-domain files ZNsatz, QNsatz, and RNsatz (#155, by Andres Erbsen).
in Permutation
- Moved Fin-specific definitons into FinFun (#154, by Andres Erbsen).
in RIneq.v
- Changed the statement of Rmult_gt_reg_l. Use the convertible Rmult_lt_reg_l if you need a backward compatible solution (#213, fixes #212, by Damien Doligez).
in ZArith,v and dependencies
- Reducing reliance on Znumtheory within stdlib changed the internal dependencies between files, code relying on files being transitively required in stdlib may need to now explicitly Require Znumtheory, BinInt, BinList, BinNat, BinNums, BinPos, Setoid, Tauto, Zhints, Zpow_def, Zpow_facts, or Zbool (#136, by Andres Erbsen).

Added 

in BinInt
- Added lemmas div_eucl_0_r, mod_0_r, div_0_r (#150, by Andres Erbsen).
in BinNatDef.v and BinNat.v
- Added definition Niter_op for repeating associative operations, a proof relating it to the generic N.iter (iter_op_correct), and properties iter_op_0_r, iter_op_1_r, iter_op_succ_r, and iter_op_add_r (#134, by Andres Erbsen).
in Diaconescu.v
- Add a proof of Diaconescu's theorem assuming propositional extensionality rather than predicate extensionality (#214, by Jean Abou Samra).
in ENsatzTactic
- Add new tactic ensatz for proving polynomial equalities with existential quantifiers or existential variables (#160, by Lionel Blatter).
in HLevelsBase.v
- transparent lemmas false_hprop, true_hprop, Is_true_hprop, eq_true_hprop, and a wrappers transparent_Is_true and transparent_eq_true to produce transparent proofs for Is_true and eq_true given not necessarily transparent proofs of the same (#133, by Andres Erbsen).
in Ncring_tac
- Added extension-point typeclass extra_reify that is only resolved on non-variables for which built-in syntax-directed reification did not find a match (#156, by Andres Erbsen).
in NsatzTactic
- Added support for nsatz using ring hypotheses above non-ring hypotheses. If a proof relies on nsatz not using earlier ring hypotheses, clear these hypotheses before calling nsatz. (#157, by Andres Erbsen).
in ZArithRing
- Added Zpower_theory to replace the now-deprecated one in Zpow_def (#150, by Andres Erbsen).
in Zcong.v
- theory of integer congruences and multiplicative inverses up to Chinese Remainder Theorem (#135, by Andres Erbsen).
new file Zdivisibility.v
- Refactored theory of integer divisibility including primality and coprimality. This file is intended to replace Znumtheory (#136, by Andres Erbsen).
in Zmod.v
- Added theory of modular integer arithmetic, including machine words / bitvectors and the multiplicative group of integers modulo another integer. About 450 lemmas are provided (#144, by Andres Erbsen).
in ZmodNsatz and Zmod
- Added support for the nsatz tactic on Zmod (#156, by Andres Erbsen).
in ZModOffset.v
- Added theory of Z.modulo with output range shifted by a constant. The main definition is Z.omodulo, with Z.smodulo capturing the special case where the offset is equal to half of the modulus, such as in two's-complement arithmetic (#135, by Andres Erbsen).

Removed 

in Zdiv.v
- alias Zmod for Z.modulo, deprecated since 8.17 (#149, by Andres Erbsen).
in ZMicromega
- Support for EnumProof`s in `ZChecker. The lia plugin does not generate such proofs anymore. If you have a different certificate generator that targets the same checker, please open an issue (#150, by Andres Erbsen).

Deprecated 

in Div
- Lemmas Zmod_0_r and Zdiv_0_r in favor of BinInt.Z.mod_0_r and BinInt.Z.div_0_r (#150, by Andres Erbsen).
in Rtauto and rtauto.Bintree
- If you use this plugin and would like to continue using it, please open an issue to discuss its maintainership (#161, by Andres Erbsen).
in ZMicromega
- Internal tactics flatten_bool and inv, definitions EnumProof, isZ0, bdepth, vars, and lemmas eq_le_iff, isZ0_0, isZ0_0, isZ0_n0, isZ0_n0, eq_true_iff_eq, max_var_le, max_var_correct, max_var_nformulae_correct_aux, max_var_nformalae_correct, ltof_bdepth_split_l, ltof_bdepth_split_r (#150, by Andres Erbsen).
- Misplaced lemma Zpower_theory, with replacement in ZArithRing (#150, by Andres Erbsen).
in Znumtheory.v
- Deprecated most definitions in favor of Zdivisibility.v or appropriate established files (#136, by Andres Erbsen).

Version 9.0

Changes in 9.0.0

Changed 

Changed the requirement prefix of the standard library from Coq to Stdlib and made it mandatory. As a temporary measure, for backward compatibility with older versions, Coq, or a missing From Stdlib, is immediatly translated to Stdlib with a warning. It is thus not recommended to name anything Coq or Coq.*. The recommended transition path is to first potentially silence the warnings, adding the lines -arg -w -arg -deprecated-from-Coq, -arg -w -arg -deprecated-dirpath-Coq and -arg -w -arg -deprecated-missing-stdlib or simply the more generic -arg -compat -arg 8.20 to your _CoqProject. Then, when droping support for Coq <= 8.20, replacing requirement of Stdlib modules by From Stdlib Require {Import,Export,} <LibraryModules>.. Beware that the Stdlib still has a handful redundant names, that is for modules Byte, you still have to use From Stdlib.Strings or From Stdlib.Init, for Tactics use From Stdlib.Program or From Stdlib.Init, for Tauto use From Stdlib.micromega or From Stdlib.Init and for Wf, use From Stdlib.Program or From Stdlib.Init (#19310 and #19530, the latter starting to implement CEP#83 by Pierre Roux).
in Fin.v
- case_L_R' and case_L_R made transparent definitions (#19655, by Andrej Dudenhefner).
in List.v
- lemmas that were using the letter O in their name to refer to zero now use instead the digit 0 (#19479, by Hugo Herbelin).
in several files
- remove transitive requirements or export of theories about Z, you may need to add explicit Require or Import of ZArith or Lia (#19801, by Andres Erbsen).
in Zbool.v
- definition of Zeq_bool is now an alias for Z.eqb, this is expected to simplify simultaneous compatibility with 8.20 and 9.0 (#19801, by Andres Erbsen).

Added 

file All.v which does Require Export of all other files in Stdlib (#19914, by Gaëtan Gilbert).
in BinPos.v
- lemma BinPos.iter_op_correct, relating Pos.iter_op for associative operations to the more general Pos.iter (#19749, by Andres Erbsen).
in Eqdep_dec.v in Logic
- lemmas UIP_None_l, UIP_None_r, UIP_None_None, UIP_nil_l, UIP_nil_r, UIP_nil_nil (#19483, by Andres Erbsen).
in EquivDec.v in Classes
- EqDec instance for option (#19949, by Daniil Iaitskov).
in Fin.v
- lemmas case_L_R'_L, case_L_R'_R, case_L_R_L, case_L_R_R (#19655, by Andrej Dudenhefner).
in Inverse_Image.v in Wellfounded
- lemmas Acc_simulation and wf_simulation (#18183, by Andrej Dudenhefner).
in List.v
- lemmas length_cons and length_nil (#19479, by Hugo Herbelin).
- Proper instance to enable setoid_rewrite to rewrite inside the function argument of List.map (#19515, by Andres Erbsen).
- lemmas length_tl, tl_map, filter_rev, filter_map_swap, filter_true, filter_false, list_prod_as_flat_map, skipn_seq, map_const, fst_list_prod, snd_list_prod, Injective_map_NoDup_in, and Permutation_map_same_l (#19748, by Andres Erbsen).
- lemma length_app_comm (#75, by Nicholas Hubbard).
file List_Extension.v in Wellfounded (#18183, by Andrej Dudenhefner).
in List_Extension.v
- well-founded list extension list_ext of a well-founded relation, including infrastructure lemmas. It can be used for well-foundedness proofs such as wf_lex_exp in Lexicographic_Exponentiation.v (#18183, by Andrej Dudenhefner).
in NatInt.v
- lemmas mul_reg_l and mul_reg_r (#17560, by Remzi Yang).
in Operators_Properties.v in Relations
- lemma clos_t_clos_rt (#18183, by Andrej Dudenhefner).
in Reals
- new file Zfloor.v with definitions of Zfloor and Zceil and corresponding lemmas up_Zfloor, IZR_up_Zfloor, Zfloor_bound, Zfloor_lub, Zfloor_eq, Zfloor_le, Zfloor_addz, ZfloorZ, ZfloorNZ, ZfloorD_cond, Zceil_eq, Zceil_le, Zceil_addz, ZceilD_cond, ZfloorB_cond, ZceilB_cond (#89, by Laurent Théry).
in VectorSpec.v
- lemma Forall2_cons_iff (#19269, by Lucas Donati and Andrej Dudenhefner and Pierre Rousselin).
in Zdiv.v
- lemma Z.mod_id_iff generalizes Z.mod_small. (#19752, by Andres Erbsen).
- lemmas Z.mod_opp_mod_opp, Z.mod_mod_opp_r, Z.mod_opp_r_mod, Z.mod_mod_abs_r, Z.mod_abs_r_mod combining Z.modulo with Z.opp or Z.abs (#19752, by Andres Erbsen).
- Lemmas cong_iff_0 and cong_iff_ex can be used to reduce congruence equalities to equations where only one side is headed by Z.modulo. (#19752, by Andres Erbsen).
- Lemmas Z.gcd_mod_l and Z.gcd_mod_r generalize Z.gcd_mod. (#19752, by Andres Erbsen).
- Lemma Z.mod_mod_divide generalizes Zmod_mod. (#19752, by Andres Erbsen).
- Lemma Z.mod_pow_l allows pushing modulo inside exponentiation (#19752, by Andres Erbsen).
file Zdiv_facts.v (#19752, by Andres Erbsen).
in Zdiv_facts.v
- lemmas Z.diveq_iff and Z.mod_diveq_iff that further genralize the same concept as Z.mod_small to known quotients other than 0. (#19752, by Andres Erbsen).
- lemmas Z.eq_mod_opp and Z.eq_mod_abs (#19752, by Andres Erbsen).
in Znat.v
- lemmas N2Z.inj_lxor, N2Z.inj_land, N2Z.inj_lor, N2Z.inj_ldiff, N2Z.inj_shiftl, and N2Z.inj_shiftr relating bitwise operations on N to those on Z (#19750, by Andres Erbsen).

Deprecated 

modules ZArith_Base and Ztac, use ZArith (or BinInt) or Lia instead (#19801, by Andres Erbsen).
in Zbool.v
- definition Zeq_bool, use Z.eqb instead. (#19801, by Andres Erbsen).

Previous versions

The standard library historically used to be distributed with Coq, please look in Coq own changelog for details about older changes.