\[\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

Version 8.20

Summary of changes

Coq version 8.20 adds a new rewrite rule mechanism along with a few new features, a host of improvements to the virtual machine, the notation system, Ltac2 and the standard library.

We highlight some of the most impactful changes here:

User-defined rewrite rules

primitive strings

A lot of work went into reducing the size of the bytecode segment, which in turn means that .vo files might now be considerably smaller.

A new version of the docker-keeper compiler to build and maintain Docker images of Coq.

Notable breaking changes:

Syntactic global references passed through the using clauses of auto-like tactics are now handled as plain references rather than interpreted terms. In particular, their typeclass arguments will not be inferred. In general, the previous behaviour can be emulated by replacing auto using foo with pose proof foo; auto.

Argument order for the Ltac2 combinators List.fold_left2 and List.fold_right2 changed to be the same as in OCaml.

Importing a module containing a mutable Ltac2 definition does not undo its mutations. Replace Ltac2 mutable foo := some_expr. with Ltac2 mutable foo := some_expr. Ltac2 Set foo := some_expr. to recover the previous behaviour.

Some renaming in the standard library. Deprecations are provided for a smooth transition.

See the Changes in 8.20.0 section below for the detailed list of changes, including potentially breaking changes marked with Changed. Coq's reference manual for 8.20, documentation of the 8.20 standard library and developer documentation of the 8.20 ML API are also available.

Théo Zimmermann with help from Ali Caglayan and Jason Gross maintained coqbot used to run Coq's CI and other pull request management tasks.

Jason Gross maintained the bug minimizer and its automatic use through coqbot.

Erik Martin-Dorel maintained the Coq Docker images and the docker-keeper compiler used to build and keep those images up to date (note that the tool is not Coq specific). Cyril Cohen, Vincent Laporte, Pierre Roux and Théo Zimmermann maintained the Nix toolbox used by many Coq projects for continuous integration.

Ali Caglayan, Emilio Jesús Gallego Arias, Rudi Grinberg and Rodolphe Lepigre maintained the Dune build system for OCaml and Coq used to build Coq itself and many Coq projects.

The opam repository for Coq packages has been maintained by Guillaume Claret, Guillaume Melquiond, Karl Palmskog and Enrico Tassi with contributions from many users. A list of packages is available on the Coq website.

Coq 8.20 was made possible thanks to the following reviewers: Frédéric Besson, Lasse Blaauwbroek, Ali Caglayan, Cyril Cohen, Andrej Dudenhefner, Andres Erbsen, Jim Fehrle, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Jason Gross, Hugo Herbelin, Ralf Jung, Jan-Oliver Kaiser, Chantal Keller, Olivier Laurent, Rodolphe Lepigre, Yishuai Li, Ralph Matthes, Guillaume Melquiond, Pierre-Marie Pédrot, Karl Palmskog, Clément Pit-Claudel, Pierre Rousselin, Pierre Roux, Michael Soegtrop, soukouki, Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi, Niels van der Weide, Nickolai Zeldovich and Théo Zimmermann. See the Coq Team face book page for more details on Coq's development team.

The 59 contributors to the 8.20 version are: Timur Aminev, Frédéric Besson, Lasse Blaauwbroek, Björn Brandenburg, Ali Caglayan, Nikolaos Chatzikonstantinou, Sylvain Chiron, chluebi, Cyril Cohen, Anton Danilkin, Louise Dubois de Prisque, Andrej Dudenhefner, Maxime Dénès, Andres Erbsen, Jim Fehrle, Davide Fissore, Andreas Florath, Yannick Forster, Mario Frank, Gaëtan Gilbert, Georges Gonthier, Jason Gross, Stefan Haan, Hugo Herbelin, Lennart Jablonka, Emilio Jesús Gallego Arias, Ralf Jung, Jan-Oliver Kaiser, Evgenii Kosogorov, Rodolphe Lepigre, Yann Leray, David M. Cooke, Erik Martin-Dorel, Guillaume Melquiond, Guillaume Munch-Maccagnoni, Karl Palmskog, Julien Puydt, Pierre-Marie Pédrot, Ramkumar Ramachandra, Pierre Rousselin, Pierre Roux, Kazuhiko Sakaguchi, Bernhard Schommer, Remy Seassau, Matthieu Sozeau, Enrico Tassi, Romain Tetley, Laurent Théry, Alexey Trilis, Oliver Turner, Quentin Vermande, Li-yao Xia and Théo Zimmermann,

The Coq community at large helped improve this new version via the GitHub issue and pull request system, the coq-club@inria.fr mailing list, the Discourse forum and the Coq Zulip chat.

Version 8.20's development spanned 7 months from the release of Coq 8.19.0 (9 months since the branch for 8.19.0). Pierre Roux and Guillaume Melquiond are the release managers of Coq 8.20. This release is the result of 470 merged PRs, closing 113 issues.

Toulouse, September 2024

Pierre Roux and Guillaume Melquiond for the Coq development team

Changes in 8.20.0

Kernel 

Changed: The guard checker now recognizes uniform parameters of a fixpoint and treats their instances as constant over the recursive call (#17986, grants #16040, by Hugo Herbelin).
Added: A mechanism to add user-defined rewrite rules to Coq's reduction mechanisms; see chapter User-defined rewrite rules (#18038, by Yann Leray).
Added: Support for primitive strings in terms (#18973, by Rodolphe Lepigre).

Specification language, type inference 

Changed: warnings future-coercion-class-constructor and future-coercion-class-field about :> in Class as errors by default. This offers a last opportunity to replace :> with :: (available since Coq 8.18) to declare typeclass instances before making :> consistently declare coercions in all records in next version. To adapt huge codebases, you can try this script or the one below. But beware that both are incomplete.

  #!/bin/awk -f
  BEGIN {
    startclass = 0;
    inclass = 0;
    indefclass = 0;  # definitionalclasses (single field, without { ... })
  }
  {
    if ($0 ~ "[ ]*Class") {
      startclass = 1;
    }
    if (startclass == 1 && $0 ~ ":=") {
      inclass = 1;
      indefclass = 1;
    }
    if (startclass == 1 && $0 ~ ":=.*{") {
      indefclass = 0;
    }
    if (inclass == 1) startclass = 0;

    if (inclass == 1 && $0 ~ ":>") {
      if ($0 ~ "{ .*:>") {  # first field on a single line
        sub("{ ", "{ #[global] ");
      } else if ($0 ~ ":=.*:>") {  # definitional classes on a single line
        sub(":= ", ":= #[global] ");
      } else if ($0 ~ "^  ") {
        sub("  ", "  #[global] ");
      } else {
        $0 = "#[global] " $0;
      }
      sub(":>", "::")
    }
  print $0;

  if ($0 ~ ".*}[.]" || indefclass == 1 && $0 ~ "[.]$") inclass = 0;
}

(#18590, by Pierre Roux).

Changed: Mutually-proved theorems with statements in different coinductive types now supported (#18743, by Hugo Herbelin).
Added: CoFixpoint supports attributes bypass_guard, clearbody, deprecated and warn (#18754, by Hugo Herbelin).
Added: Program Fixpoint with measure or wf (see Program Fixpoint) now supports the where clause for notations, the local and clearbody attributes, as well as non-atomic conclusions (#18834, by Hugo Herbelin, fixes in particular #13812 and #14841).
Fixed: Anomaly on the absence of remaining obligations of some name now an error (#18873, fixes #3889, by Hugo Herbelin).
Fixed: Universe polymorphic Program's obligations are now generalized only over the universe variables that effectively occur in the obligation (#18915, fixes #11766 and #11988, by Hugo Herbelin).
Fixed: Anomaly assertion failed in pattern-matching compilation, with Program Mode or with let-ins in the arity of an inductive type (#18921, fixes #5777 and #11030 and #11586, by Hugo Herbelin).
Fixed: Support for Program-style pattern-matching on more than one argument in an inductive family (#18929, fixes #1956 and #5777, by Hugo Herbelin).
Fixed: anomaly with obligations in the binders of a measure- or wf-based Program Fixpoint (#18958, fixes #18920, by Hugo Herbelin).
Fixed: Incorrect registration of universe names attached to a primitive polymorphic constant (#19100, fixes #19099, by Hugo Herbelin).

Notations 

Changed: an only printing interpretation of a notation with a specific format does no longer change the printing rule of other interpretations of the notation; to globally change the default printing rule of all interpretations of a notation, use Reserved Notation instead (#16329, fixes #16262, by Hugo Herbelin).
Changed: levels of Reserved Notation now default to levels of previous notations with longest common prefix, if any. This helps to factorize notations with common prefixes (#19149, by Pierre Roux).
Added: closed-notation-not-level-0 and postfix-notation-not-level-1 warnings about closed and postfix notations at unusual levels (#18588, by Pierre Roux).
Added: notation-incompatible-prefix warning when two notation definitions have incompatible prefixes (#19049, by Pierre Roux).
Fixed: Notations for applied constants equipped with multiple signatures of implicit arguments were not correctly inserting as many maximal implicit arguments as they should have (#18445, by Hugo Herbelin).
Fixed: Add support for printing notations applied to extra arguments in custom entries, thus eliminating an anomaly (#18447, fixes #18342, by Hugo Herbelin).

Tactics 

Changed: When using Z.to_euclidean_division_equations, nia can now relate Z.div/Z.modulo to Z.quot/Z.rem a bit better, by virtue of being noticing when there are two equations of the form x = y * q₁ + _ and x = y * q₂ + _ (or minor variations thereof), suggesting that q₁ = q₂. Users can replace Z.to_euclidean_division_equations with let flags := Z.euclidean_division_equations_flags.default_with Z.euclidean_division_equations_flags.find_duplicate_quotients false in Z.to_euclidean_division_equations_with flags or, using Import Z.euclidean_division_equations_flags., with Z.to_euclidean_division_equations_with ltac:(default_with find_duplicate_quotients false) (#17934, by Jason Gross).
Changed: The opacity/transparency of primitive projections is now attached to the projections themselves, not the compatibility constants, and compatibility constants are always considered transparent (#18327, fixes #18281, by Jan-Oliver Kaiser and Rodolphe Lepigre).
Changed: Tactic intro z on an existential variable goal forces the resolution of the existential variable into a goal forall z:?T, ?P, which becomes ?P in context z:?T after introduction. The existential variable ?P itself is now defined in a context where the variable of type ?T is also named z, as specified by intro instead of x as it was conventionally the case before (#18395, by Hugo Herbelin).
Changed: syntactic global references passed through the using clauses of auto-like tactics are now handled as plain references rather than interpreted terms. In particular, their typeclass arguments will not be inferred. In general, the previous behaviour can be emulated by replacing auto using foo with pose proof foo; auto (#18909, by Pierre-Marie Pédrot).
Changed: Use Coqlib's Register mechanism for the generalized rewriting tactic and make the (C)RelationClasses/(C)Morphisms independent of the rewrite tactic to ease maintainance. (#19115, by Matthieu Sozeau).
Removed: the clear modifier which was deprecated since 8.17 (#18887, by Pierre-Marie Pédrot).
Removed: the cutrewrite tactic, which was deprecated since Coq 8.5 (#19027, by Pierre-Marie Pédrot).
Deprecated: non-reference hints in using clauses of auto-like tactics (#19006, by Pierre-Marie Pédrot).
Deprecated: the gintuition tactic, which used to be undocumented until Coq 8.16 (#19129, by Pierre-Marie Pédrot).
Deprecated: destauto, see #11537 (#19179, by Jim Fehrle).
Added: When using Z.to_euclidean_division_equations, you can now pose equations of the form x = y * q using Z.divide (#17927, by Evgenii Kosogorov).
Added: support for Nat.double and Nat.div2 to zify and lia (#18729, by Andres Erbsen).
Added: the replace tactic now accepts -> and <- to specify the direction of the replacement when used with a with clause (#19060, fixes #13480, by Pierre-Marie Pédrot).
Fixed: The name of a cofixpoint globally defined with a name is now systematically reused by simpl after reduction, even when the named cofixpoint is mutually defined or defined in a section (#18576, fixes #4056, by Hugo Herbelin).
Fixed: The reduction of primitive projections of cofixpoints by simpl is now implemented (#18577, fixes #7982, by Hugo Herbelin).
Fixed: Support for refolding reduced global mutual fixpoints/cofixpoints with parameters in cbn (#18601, fixes part of #4056, by Hugo Herbelin).
Fixed: cbn was leaving behind unnamable constants when refolding mutual fixpoints/cofixpoints from aliased modules (#18616, fixes #17897, by Hugo Herbelin).
Fixed: cbv of primitive projections applied to a tuple now ignores beta like it does for cbn, lazy and simpl (#18618, fixes #9086, by Hugo Herbelin).

Ltac language 

Added: In rewrite_strat, rewstrategy now supports the fixpoint operator fix ident := rewstrategy1 (#18094, fixes #13702, by Jason Gross and Gaëtan Gilbert).
Fixed: rewrite_strat now works inside module functors (#18094, fixes #18463, by Jason Gross).

Ltac2 language 

Changed: recursive let and non mutable projections of syntactic values are considered syntactic values (#18411, by Gaëtan Gilbert).
Changed: Ltac2 are typechecked at declaration time by default. This should produce better errors when a notation argument does not have the expected type (e.g. wrong branch type in match! goal). In the previous behaviour of typechecking, only the expansion result can be recovered using Ltac2 Typed Notations. We believe there are no real use cases for this, please report if you have any (#18432, fixes #17477, by Gaëtan Gilbert).
Changed: argument order for the Ltac2 combinators List.fold_left2 and List.fold_right2 changed to be the same as in OCaml (#18706, by Gaëtan Gilbert).
Changed: Importing a module containing a mutable Ltac2 definition does not undo its mutations. Replace Ltac2 mutable foo := some_expr. with Ltac2 mutable foo := some_expr. Ltac2 Set foo := some_expr. to recover the previous behaviour (#18713, by Gaëtan Gilbert).
Changed: the using clause argument of auto-like tactics in Ltac2 now take a global reference rather than arbitrary constr (#18940, by Pierre-Marie Pédrot).
Deprecated: Ltac2.Constr.Pretype.Flags.open_constr_flags whose name is misleading as it runs typeclass inference unlike open_constr:() (#18765, by Gaëtan Gilbert).
Added: fst and snd in Ltac2.Init (#18370, by Gaëtan Gilbert).
Added: Ltac2.Ltac1.of_preterm and to_preterm (#18551, by Gaëtan Gilbert).
Added: of_intro_pattern and to_intro_pattern in Ltac2.Ltac1 (#18558, by Gaëtan Gilbert).
Added: basic APIs in Ltac2.Ltac1 to produce slightly more informative errors when failing to convert a Ltac1 value to some Ltac2 type (#18558, by Gaëtan Gilbert).
Added: APIs Ltac2.Control.unshelve and Ltac2.Notations.unshelve (#18604, by Gaëtan Gilbert).
Added: warning on unused Ltac2 variables (except when starting with _) (#18641, by Gaëtan Gilbert).
Added: Ltac2.Control.numgoals (#18690, by Gaëtan Gilbert).
Added: intropattern and intropatterns notation scopes support views (foo%bar) (#18757, by Gaëtan Gilbert).
Added: open recursion combinators in Ltac2.Constr.Unsafe (#18764, by Gaëtan Gilbert).
Added: APIs in Ltac2.Constr.Pretype.Flags to customize pretyping flags. (#18765, by Gaëtan Gilbert).
Added: abstract attribute for Ltac2 Type to turn types abstract at the end of the current module (#18766, fixes #18656, by Gaëtan Gilbert).
Added: APIs in Ltac2.Message to interact with the boxing system of the pretty printer (#18988, by Gaëtan Gilbert).
Added: Automatic Proposition Inductives, Dependent Proposition Eliminators and warning when automatically lowering an inductive declared with Type to Prop (#18989, by Gaëtan Gilbert).
Added: String.sub (#19204, by Rodolphe Lepigre).
Fixed: Ltac2.Control.new_goal removes the new goal from the shelf and future goals (#19141, fixes #19138, by Gaëtan Gilbert).

SSReflect 

Changed: ssreflect no longer relies on the recovery mechanism of the parsing engine, this can slightly change the parsing priorities in rare occurences, for instance when combining unshelve and => (#18224, by Pierre Roux).
Changed: notations _.1 and _.2 are now defined in the prelude at level 1 rather than in ssrfun at level 2 (#18224, by Pierre Roux).
Changed: The have tactic generates a proof term containing an opaque constant, as it did up to PR #15121 included in Coq 8.16.0. See the variant have @H to generate a (transparent) let-in instead (Generating let in context entries with have). (#18449, fixes #18017, by Enrico Tassi).
Deprecated: The fun_scope notation scope declared in ssrfun.v is deprecated. Use function_scope instead (#18374, by Kazuhiko Sakaguchi).
Fixed: handling of primitive projections in ssrewrite (#19213, fixes #19229, by Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi and Quentin Vermande).

Commands and options 

Changed: the default reversibility status of most coercions. The refman states that

By default coercions are not reversible except for Record fields specified using :>.

The previous code was making way too many coercion reversible by default. The new behavior should be closer from the spec in the doc (#18705, by Pierre Roux).
Changed: focus commands such as 1:{ and goal selection for query commands such as 1: Check do not need Classic (Ltac1) proof mode to function. In particular they function in Ltac2 mode (#18707, fixes #18351, by Gaëtan Gilbert).
Changed: inductives declared with : Type or no annotation and automatically put in Prop are not declared template polymorphic (#18867, by Gaëtan Gilbert).
Changed: Clarify the warning about use of Let, Variable, Hypothesis and Context outside sections and make it an error by default (#18880, by Pierre Roux).
Changed: The "fragile-hint-constr" warning is now an error by default, as the corresponding feature will be removed in a later version (#18895, by Pierre-Marie Pédrot).
Changed: Scheme automatically registers the resulting schemes in the Register Scheme database (#19016, fixes #3132, by Gaëtan Gilbert).
Changed: Typeclasses Transparent and Typeclasses Opaque default locality outside section is now export (#19069, by Gaëtan Gilbert).
Deprecated: The Cd command. Instead use the command line option -output-directory (see Command line options) or, for extraction, Extraction Output Directory (#17403, by Ali Caglayan and Hugo Herbelin).
Added: warn attribute generalizing the deprecation machinery to other forms of comments (#18248, by Hugo Herbelin and Pierre Roux).
Added: Register Scheme to add entries to the scheme database used by some tactics (#18299, by Gaëtan Gilbert).
Added: Print reference now shows the implicit arguments of a reference directly on the type of reference, using {...} and [...] markers for respectively maximally-inserted and non-maximally-inserted implicit arguments, as About does (#18444, by Hugo Herbelin).
Added: import_categories supports category options controlling Flags, Options and Tables (#18536, by Gaëtan Gilbert).
Added: When a name is a projection, About and Print now indicate it (#18725, by Hugo Herbelin).
Added: Hint Projections command that sets the transparency flag for projections for the specified hint databases (#18785, by Jan-Oliver Kaiser and Rodolphe Lepigre).
Added: Search now admits the is:Fixpoint and is:CoFixpoint logical kinds to search for constants defined with the Fixpoint and CoFixpoint keywords (#18983, by Pierre Rousselin).
Added: The Include command can now include module types with a with clause (with_declaration) to instantiate some parameters (#19144, by Pierre Rousselin).
Fixed: Fixes missing implicit arguments coming after a -> in the main type printed by Print and About (#18442, fixes #15020, by Hugo Herbelin).
Fixed: Cumulativity Weak Constraints can unify universes to Set when Universe Minimization ToSet is enabled (#18458, by Gaëtan Gilbert).
Fixed: Search with modifier is:Scheme restricted the search to inductive types which have schemes instead of the schemes themselves. For instance Search nat is:Scheme with just the prelude loaded would return le i.e. the only inductive type whose type mentions nat (#18537, fixes #18298, by Gaëtan Gilbert).
Fixed: Search now searches also in included module types (#18662, fixes #18657, by Hugo Herbelin).
Fixed: Eval and Definition with := Eval work without needing to load the Ltac plugin (#18852, fixes #12948, by Gaëtan Gilbert).
Fixed: Scheme declares non-recursive schemes for scheme_type Case and Elimination (#19017, fixes #10816, by Gaëtan Gilbert).
Fixed: Cumulativity Weak Constraints had its meaning flipped since 8.12 (#19201, by Gaëtan Gilbert).

Command-line tools 

Changed: signal SIGINT interrupts the process with " "user interrupt" error instead of aborting. This is intended to produce better messages when interrupting Coq (#18716, by Gaëtan Gilbert).
Added: Command line option -output-directory dir to set the default output directory for extraction, Redirect and Print Universes (#17392, fixes #8649, by Hugo Herbelin).
Fixed: coqdoc links to section variables introduced with Context (#18527, fixes #18516, by Pierre Roux).

CoqIDE 

Changed: Find/replace UI was improved: margins, icons for found/not found (#18523, fixes #11024, by Sylvain Chiron).
Changed: The default key binding modifier for the Navigation menu was changed to Alt on non-macOS systems. The previous default, Ctrl, hid some conventional cursor movement bindings such as Ctrl-Left, Ctrl-Right, Ctrl-Home and Ctrl-End. The new default generally has no effect if you've previously installed Coq on your system. See Shortcuts to change the default.

The Edit/Undo key binding was changed from Ctrl-U to Ctrl-Z to be more consistent with common conventions. View/Previous Tab and View/Next Tab were changed from Alt-Left/Right to Ctrl-PgUp/PgDn (Cmd-PgUp/PgDn on macOS). To change key bindings on your system (e.g. back to Ctrl-U), see Key bindings (#18717, by Sylvain Chiron).
Changed: Changing modifiers for the View menu only applies to toggleable items; View/Show Proof was changed to Shift-F2 (#18717, by Sylvain Chiron).
Added: Edit/Select All and Navigation/Fully Check menu items (#18717, fixes #16141, by Sylvain Chiron).
Fixed: Opening a file with drag and drop now works correctly (fixed regression) (#18524, fixes #3977, by Sylvain Chiron).
Fixed: Incorrect highlight locations and line numbers for errors and warnings, especially in the presence of unicode characters. This updates the XML protocol (#19040, fixes #18682, by Hugo Herbelin).
Fixed: Show tooltips for syntax errors (#19153, fixes #19152, by Jim Fehrle).

Standard library 

Changed: names of "push" lemmas for List.length to follow the same convention as push lemmas for other operations. For example, app_length became length_app. The standard library was migrated using the following script:

find theories -name '*.v' | xargs sed -i -E '
  s/\<app_length\>/length_app/g;
  s/\<rev_length\>/length_rev/g;
  s/\<map_length\>/length_map/g;
  s/\<fold_left_length\>/fold_left_S_O/g;
  s/\<split_length_l\>/length_fst_split/g;
  s/\<split_length_r\>/length_snd_split/g;
  s/\<combine_length\>/length_combine/g;
  s/\<prod_length\>/length_prod/g;
  s/\<firstn_length\>/length_firstn/g;
  s/\<skipn_length\>/length_skipn/g;
  s/\<seq_length\>/length_seq/g;
  s/\<concat_length\>/length_concat/g;
  s/\<flat_map_length\>/length_flat_map/g;
  s/\<list_power_length\>/length_list_power/g;
'

(#18564, by Andres Erbsen).

Changed: Coq.CRelationClasses.arrow, Coq.CRelationClasses.iffT and Coq.CRelationClasses.flip are now Typeclasses Opaque (#18910, by Pierre-Marie Pédrot).
Removed: The library files Coq.NArith.Ndigits, Coq.NArith.Ndist, and Coq.Strings.ByteVector which were deprecated since 8.19 (#18936, by Andres Erbsen).
Deprecated: The library files
- Coq.Numbers.Integer.Binary.ZBinary
- Coq.Numbers.Integer.NatPairs.ZNatPairs
- Coq.Numbers.Natural.Binary.NBinary
have been deprecated. Users should require Coq.Arith.PeanoNat or Coq.Arith.NArith.BinNat if they want implementations of natural numbers and Coq.Arith.ZArith.BinInt if they want an implementation of integers (#18500, by Pierre Rousselin).
Deprecated: The library file Coq.Numbers.NatInt.NZProperties is deprecated. Users can require Coq.Numbers.NatInt.NZMulOrder instead and replace the module NZProperties.NZProp with NZMulOrder.NZMulOrderProp (#18501, by Pierre Rousselin).
Deprecated: The library file Coq.Arith.Bool_nat has been deprecated (#18538, by Pierre Rousselin).
Deprecated: The library file Coq.Numbers.NatInt.NZDomain is deprecated (#18539, by Pierre Rousselin).
Deprecated: The library files Coq.Numbers.Integers.Abstract.ZDivEucl and Coq.ZArith.Zeuclid are deprecated (#18544, by Pierre Rousselin).
Deprecated: The library files Coq.Numbers.Natural.Abstract.NIso and Coq.Numbers.Natural.Abstract.NDefOps are deprecated (#18668, by Pierre Rousselin).
Deprecated: Bool.Bvector. Users are encouraged to consider list bool instead. Please open an issue if you would like to keep using Bvector. (#18947, by Andres Erbsen).
Added: A warning on Vector.t to make its new users aware that using this dependently typed representation of fixed-length lists is more technically difficult, compared to bundling lists with a proof of their length. This is not a deprecation and there is no intent to remove it from the standard library. Use option -w -stdlib-vector to silence the warning (#18032, by Pierre Roux, reviewed by Andres Erbsen, Jim Fehrle, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Hugo Herbelin, Olivier Laurent, Yishuai Li, Pierre-Marie Pédrot and Michael Soegtrop).
Added: lemmas NoDup_app, NoDup_iff_ForallOrdPairs, NoDup_map_NoDup_ForallPairs and NoDup_concat (#18172, by Stefan Haani and Andrej Dudenhefner).
Added: lemmas In_iff_nth_error nth_error_app, nth_error_cons_0, nth_error_cons_succ, nth_error_rev, nth_error_firstn, nth_error_skipn, hd_error_skipn, nth_error_seq (#18563, by Andres Erbsen)
Added: to N and Nat lemmas strong_induction_le, binary_induction, strong_induction_le, even_even, odd_even, odd_odd, even_odd, b2n_le_1, testbit_odd_succ', testbit_even_succ', testbit_div2, div2_0, div2_1, div2_le_mono, div2_even, div2_odd', le_div2_diag_l, div2_le_upper_bound, div2_le_lower_bound, lt_div2_diag_l, le_div2, lt_div2, div2_decr, land_even_l, land_even_r, land_odd_l, land_odd_r, land_even_even, land_odd_even, land_even_odd, land_odd_odd, land_le_l, land_le_r, ldiff_even_l, ldiff_odd_l, ldiff_even_r, ldiff_odd_r, ldiff_even_even, ldiff_odd_even, ldiff_even_odd, ldiff_odd_odd, ldiff_le_l, shiftl_lower_bound, shiftr_upper_bound, ones_0, ones_succ, pow_lower_bound (#18628, by Pierre Rousselin).
Fixed: Z.euclidean_division_equations_cleanup has been reordered so that zify (and lia, nia, etc) are no longer as slow when the context contains many assumptions of the form 0 <= ... < ... (#18818, fixes #18770, by Jason Gross).

Infrastructure and dependencies 

Changed: Bump minimal Dune version required to build Coq to 3.6.1 (#18359, by Emilio Jesus Gallego Arias).
Removed: Support for .vio files and for .vio2vo transformation has been removed, compilation to .vos is the supported method for quick compilation now (#18424, fixes #4007 and #4013 and #4123 and #5308 and #5223 and #6720 and #8402 and #9637 and #11471 and #18380, by Emilio Jesus Gallego Arias).
Added: The coq-doc opam / Dune package will now build and install Coq's documentation (#17808, by Emilio Jesus Gallego Arias).
Added: Coq is now compatible with memprof-limits interruption methods. This means that Coq will be recompiled when the library is installed / removed from an OPAM switch. (#18906, fixes #17760, by Emilio Jesus Gallego Arias).
Added: ability to exit from Drop. in Coq toplevel by a simple Ctrl + D, without leaving the OCaml toplevel on the stack. Also add a custom OCaml toplevel directory #go which does the same action as go (), but with a more native syntax (#18771, by Anton Danilkin).

Extraction 

Added: Extension for OCaml extraction: Commands to extract foreign function calls to C (external) and ML function exposition (Callback.register) for calling being able to call them by C functions (#18270, fixes #18212, by Mario Frank).
Fixed: Wrongly self-referencing extraction of primitive projections to OCaml in functors (#17321, fixes #16288, by Hugo Herbelin). Note that OCaml wrappers assuming that the applicative syntax of projections is provided may have to use the dot notation instead.

Version 8.19

Summary of changes

Coq version 8.19 extends the kernel universe polymorphism to polymorphism over sorts (e.g. Prop, SProp) along with a few new features, a host of improvements to the notation system, the Ltac2 standard library, and the removal of some standard library files after a long deprecation period.

We highlight some of the most impactful changes here:

Sort polymorphism makes it possible to share common constructs over Type Prop and SProp.

The notation term%_scope to set a scope only temporarily (in addition to term%scope for opening a scope applying to all subterms).

lazy, simpl, cbn and cbv and the associated Eval and eval reductions learned to do head reduction when given flag head.

New Ltac2 APIs, improved Ltac2 exact and dynamic building of Ltac2 term patterns.

New performance evaluation facilities: Instructions to count CPU instructions used by a command (Linux only) and Profiling system to produce trace files.

New command Attributes to assign attributes such as deprecated to a library file.

Notable breaking changes:

replace with by tac does not automatically attempt to solve the generated equality subgoal using the hypotheses. Use by first [assumption | symmetry;assumption | tac] if you need the previous behaviour.

Removed old deprecated files from the standard library.

See the Changes in 8.19.0 section below for the detailed list of changes, including potentially breaking changes marked with Changed. Coq's reference manual for 8.19, documentation of the 8.19 standard library and developer documentation of the 8.19 ML API are also available.

Maxime Dénès and Thierry Martinez with support from Erik Martin-Dorel and Théo Zimmermann moved the CI away from gitlab.com to use Inria supported runner machines through gitlab.inria.fr.

Théo Zimmermann with help from Ali Caglayan and Jason Gross maintained coqbot used to run Coq's CI and other pull request management tasks.

Jason Gross maintained the bug minimizer and its automatic use through coqbot.

Jaime Arias and Erik Martin-Dorel maintained the Coq Docker images and Cyril Cohen, Vincent Laporte, Pierre Roux and Théo Zimmermann maintained the Nix toolbox used by many Coq projects for continuous integration.

Ali Caglayan, Emilio Jesús Gallego Arias, Rudi Grinberg and Rodolphe Lepigre maintained the Dune build system for OCaml and Coq used to build Coq itself and many Coq projects.

The opam repository for Coq packages has been maintained by Guillaume Claret, Guillaume Melquiond, Karl Palmskog and Enrico Tassi with contributions from many users. A list of packages is available on the Coq website.

Our current maintainers are Yves Bertot, Frédéric Besson, Ana Borges, Ali Caglayan, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Andres Erbsen, Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann. See the Coq Team face book page for more details.

The 40 contributors to the 8.19 version are: quarkcool, Khalid Abdullah, Tanaka Akira, Isaac van Bakel, Frédéric Besson, Lasse Blaauwbroek, Ana Borges, Ali Caglayan, Nikolaos Chatzikonstantinou, Maxime Dénès, Andrej Dudenhefner, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Jason Gross, Stefan Haan, Hugo Herbelin, Emilio Jesús Gallego Arias, Pierre Jouvelot, Ralf Jung, Jan-Oliver Kaiser, Robbert Krebbers, Jean-Christophe Léchenet, Rodolphe Lepigre, Yann Leray, Yishuai Li, Guillaume Melquiond, Guillaume Munch-Maccagnoni, Sotaro Okada, Karl Palmskog, Pierre-Marie Pédrot, Jim Portegies, Pierre Rousselin, Pierre Roux, Michael Soegtrop, David Swasey, Enrico Tassi, Shengyi Wang and Théo Zimmermann.

The Coq community at large helped improve this new version via the GitHub issue and pull request system, the coq-club@inria.fr mailing list, the Discourse forum and the Coq Zulip chat.

Version 8.19's development spanned 4 months from the release of Coq 8.18.0 (6 months since the branch for 8.18.0). Gaëtan Gilbert and Matthieu Sozeau are the release managers of Coq 8.19. This release is the result of 285 merged PRs, closing 70 issues.

Nantes, January 2024

Gaëtan Gilbert for the Coq development team

Changes in 8.19.0

Kernel 

Added: Sort polymorphism makes it possible to share common constructs over Type Prop and SProp (#17836, #18331, by Gaëtan Gilbert).
Fixed: Primitives being incorrectly considered convertible to anything by module subtyping (#18507, fixes #18503, by Gaëtan Gilbert).

Specification language, type inference 

Changed: term_forall_or_fun, term_let, term_fix, term_cofix and term_if from term at level 200 to term10 at level 10. This is a first step towards getting rid of the recovery mechanism of camlp5/coqpp. The impact will mostly be limited to rare cases of additional parentheses around the above (#18014, by Hugo Herbelin).
Changed: Declarations of the form (id := body) in Context outside a section in a Module Type do not any more try to declare a class instance. Assumptions whose type is a class and declared using Context outside a section in a Module Type are now declared as global, instead of local (#18254, by Hugo Herbelin).
Fixed: Anomaly in the presence of duplicate variables within a disjunctive pattern (#17857 and #18005, fixes #17854 and #18004, by Hugo Herbelin).
Fixed: Printing of constructors and of in clause of match now respects the Printing Implicit and Printing All flags (#18176, fixes #18163, by Hugo Herbelin).
Fixed: Wrong shift of argument names when using Arguments in nested sections (#18393, fixes #12755 and #18392, by Hugo Herbelin).

Notations 

Changed: More informative message when a notation cannot be intepreted as a reference (#18104, addresses #18096, by Hugo Herbelin).
Changed: In casts like term : t where t is bound to some scope t_scope, via Bind Scope, the term is now interpreted in scope t_scope. In particular when t is Type the term is interpreted in type_scope and when t is a product the term is interpreted in fun_scope (#6134, fixes #14959, by Hugo Herbelin, reviewed by Maxime Dénès, Jim Fehrle, Emilio Gallego, Gaëtan Gilbert, Jason Gross, Pierre-Marie Pédrot, Pierre Roux, Bas Spitters and Théo Zimmermann).
Added: the notation term%_scope to set a scope only temporarily (in addition to term%scope for opening a scope applying to all subterms) (#14928, fixes #11486 and #12157 and #14305, by Hugo Herbelin, reviewed by Pierre Roux).
Removed the ability to declare scopes whose name starts with _ (would be ambiguous with the new %_scope notation) (#14928, by Pierre Roux, reviewed by Hugo Herbelin).
Deprecated the notation term%scope in Arguments command. In a few version, we'll make it an error and in next version give it the same semantics as in terms (i.e., deep scope opening for all subterms rather than just temporary opening) (#14928, fixes #11486 and #12157 and #14305, by Hugo Herbelin, reviewed by Pierre Roux).
Added: Quoted strings can be used as tokens in notations; double quotes can be used in symbols in only printing notations; see Basic notations for details (#17123, by Hugo Herbelin).
Added: Parsing support for notations with recursive binders involving not only variables bound by fun or forall but also by let or match (#17856, fixes #17845, by Hugo Herbelin).
Added: Declaring more than once the level of a notation variable is now an error (#17988, fixes #17985, by Hugo Herbelin).
Fixed: Various bugs and limitations to using custom binders in non-recursive and recursive notations (#17115, fixes parts of #17094, by Hugo Herbelin).
Fixed: An invalid case of eta-expansion in notation pretty-printer (#17841, fixes #15221, by Hugo Herbelin).
Fixed: Printing Parentheses now works also when an explicit level is set for the right-hand side of a right-open notation (#17844, fixes #15322, by Hugo Herbelin).
Fixed: anomaly when a notation variable denoting a binder occurs nested more than once in a recursive pattern (#17861, fixes #17860, by Hugo Herbelin).
Fixed: Anomaly when trying to disable a non-existent custom notation (#17891, fixes #17782, by Hugo Herbelin).
Fixed: appropriate error instead of anomaly in the presence of notations with constructors applied to too many arguments in pattern-matching (#17892, fixes #17071, by Hugo Herbelin).
Fixed: support constructors with parameters in number or string notations for patterns (#17902, fixes #11237, by Hugo Herbelin).
Fixed: Chains of entry coercions possibly printed in the wrong order depending on the order in which they were declared (#18230, fixes #18223, by Hugo Herbelin).

Tactics 

Changed: open_constr in Ltac1 and Ltac2 does not perform evar normalization. Normalization may be recovered using let c := open_constr:(...) in constr:(c) if necessary for performance (#17704, by Gaëtan Gilbert).
Changed: abstract now supports existential variables (#17745, by Gaëtan Gilbert).
Changed: instances declared with Typeclasses Unique Instances do not allow backtracking even when the goal contains evars (#17789, fixes #6714, by Jan-Oliver Kaiser).
Changed: In rewrite_strat, the syntax for the choice strategy has changed slightly. You may need to add parentheses around its arguments (one such case found in our continuous integration tests) (#17832, by Hugo Herbelin, Jim Fehrle and Jason Gross).
Changed: replace with by tac does not automatically attempt to solve the generated equality subgoal using the hypotheses. Use by first [assumption | symmetry;assumption | tac] if you need the previous behaviour (#17964, fixes #17959, by Gaëtan Gilbert).
Changed: Z.euclidean_division_equations_cleanup now breaks up hypotheses of the form 0 <= _ < _ for better cleanup in zify (#17984, by Jason Gross).
Changed: simpl now refolds applied constants unfolding to reducible fixpoints into the original constant even when this constant would become partially applied (#17991, by Hugo Herbelin).
Added: Ltac2 tactic Std.resolve_tc to resolve typeclass evars appearing in a given term (#13071, by Gaëtan Gilbert and Maxime Dénès).
Added: lazy, simpl, cbn and cbv and the associated Eval and eval reductions learned to do head reduction when given flag head (eg Eval lazy head in (fun x => Some ((fun y => y) x)) 0 produces Some ((fun y => y) 0)) (#17503, by Gaëtan Gilbert; cbv case added in #18190, by Hugo Herbelin).
Fixed: ensure that opaque primitive projections are correctly handled by "Evarconv" unification (#17788, fixes #17774, by Rodolphe Lepigre).
Fixed: Useless duplications with Hint Cut and Hint Mode (#17887, fixes #17417, by Hugo Herbelin).
Fixed: zify / Z.euclidean_division_equations_cleanup now no longer instantiates dependent hypotheses. This will by necessity make Z.to_euclidean_division_equations a bit weaker, but the previous behavior was overly sensitive to hypothesis ordering. See #17935 for a recipe to recapture the power of the previous behavior in a more robust albeit slower way (#17935, fixes #17936, by Jason Gross).
Fixed: simpl now working on reducible named mutual fixpoints with parameters (#17993, fixes #12521 and part of #3488, by Hugo Herbelin).
Fixed: support for reasoning up to polymorphic universe variables in congruence and f_equal (#18106, fixes #5481 and #9979, by Hugo Herbelin).
Fixed: Only run zify saturation on existing hypotheses of the goal (#18152, fixes #18151, by Frédéric Besson and Rodolphe Lepigre).
Fixed: A stack overflow due to a non-tail recursive function in lia (#18159, fixes #18158, by Jan-Oliver Kaiser and Rodolphe Lepigre).
Fixed: Apply substitution in Case stack node for cbv reify (#18195, fixes #18194, by Yann Leray).
Fixed: Anomaly of simpl on partially applied named mutual fixpoints (#18243, fixes #18239, by Hugo Herbelin).
Changed: simpl tries to reduce named mutual fixpoints also when they return functions (#18243, by Hugo Herbelin).

Ltac language 

Fixed: Fix broken "r <num>" and "r <string>" commands in the coqtop Ltac debugger, which also affected the Proof General Ltac debugger (#18068, fixes #18067, by Jim Fehrle).

Ltac2 language 

Changed: Array.empty, Message.Format.stop and Pattern.empty_context are not thunked (#17534, by Gaëtan Gilbert).
Changed: Ltac2 exact and eexact elaborate their argument using the type of the goal as expected type, instead of elaborating with no expected type then unifying the resulting type with the goal (#18157, fixes #12827, by Gaëtan Gilbert).
Changed: argument order for the Ltac2 combinators List.fold_left List.fold_right and Array.fold_right changed to be the same as in OCaml (#18197, fixes #16485, by Gaëtan Gilbert).
Changed: Ltac2.Std.red_flags added field rStrength to support head-only reduction (#18273, fixes #18209, by Gaëtan Gilbert).
Added: Ltac2 supports pattern quotations when building pattern values. This allows building dynamic patterns, eg Ltac2 eq_pattern a b := pattern:($pattern:a = $pattern:b) (#17667, by Gaëtan Gilbert).
Added: new standard library modules Ltac2.Unification and Ltac2.TransparentState providing access to "Evarconv" unification, including the configuration of the transparency state (#17777, by Rodolphe Lepigre).
Added: Ltac2.Constr.is_float, Ltac2.Constr.is_uint63, Ltac2.Constr.is_array (#17894, by Jason Gross).
Added: new Ltac2 standard library modules Ltac2.Ref, Ltac2.Lazy and Ltac2.RedFlags
Added: new Ltac2 standard library functions to Ltac2.Control, Ltac2.Array, and Ltac2.List (#18095, fixes #10112, by Rodolphe Lepigre).
Added: Support for the setoid_rewrite tactic (#18102, by quarkcool).
Added: Ltac2 Globalize and Ltac2 Check useful to investigate the expansion of Ltac2 notations (#18139, by Gaëtan Gilbert).
Added: A new flag Ltac2 In Ltac1 Profiling (unset by default) to control whether Ltac2 stack frames are included in Ltac profiles (#18293, by Rodolphe Lepigre).
Added: Ltac2.Message.Format.ikfprintf useful to implement conditional printing efficiently (i.e. without building an unused message when not printing) (#18311, fixes #18292, by Gaëtan Gilbert).
Fixed: Ltac2 mutable references are not considered values anymore (#18082, by Gaëtan Gilbert).

Commands and options 

Changed: Let with Qed produces an opaque side definition instead of being treated as a transparent let after the section is closed. The previous behaviour can be recovered using clearbody and Defined (#17576, by Gaëtan Gilbert).
Changed: automatic lowering of record types to Prop now matches the behavior for inductives: no lowering when universe polymorphism is on, more lowering with recursive records (#17795, fixes #17801 and #17796 and #17801 and #17805, by Gaëtan Gilbert).
Added: Extraction Output Directory option for specifying the directory in which extracted files are written (#16126, fixes #9148, by Ali Caglayan).
Added: -profile command line argument and PROFILE variable in coq_makefile to control a new Profiling system (#17702, by Gaëtan Gilbert).
Added: new command modifier Instructions that executes the given command and displays the number of CPU instructions it took to execute it. This command is currently only supported on Linux systems, but it does not fail on other systems, where it simply shows an error message instead of the count. (#17744, by Rodolphe Lepigre).
Added: support for instruction counts to the -profile option. (#17744, by Rodolphe Lepigre).
Added: New command Attributes to assign attributes such as deprecated to a library file (#18193, fixes #8032, by Hugo Herbelin).
Fixed: Anomaly with Search in the context of a goal (#17987, fixes #17963, by Hugo Herbelin).
Fixed: The printer for Guarded was possibly raising an anomaly in the presence of existential variables (#18008, fixes #18006, by Hugo Herbelin).

Command-line tools 

Changed: Add a coqdep option -w to adjust warnings and allow turning then into errors like the corresponding coqc option (#17946, fixes #10156, by David Swasey and Rodolphe Lepigre).
Fixed: properly delayed variable expansion when coq_makefile uses the combined rule for .vo and .glob targets, i.e. on GNU Make 4.4 and later. (#18077, fixes #18076, by Gaëtan Gilbert).
Fixed: Spurious coqdep warnings due to missing path normalization for plugins (#18165, by Rodolphe Lepigre).
Fixed: Regression in option --external of coqdoc, whose two arguments were inadvertently swapped (#18448, fixes #18434, by Hugo Herbelin).

Standard library 

Changed: reimplemented Ncring_tac reification (used by nsatz, cring, but not ring) in Ltac instead of typeclasses (#18325, by Gaëtan Gilbert).
Removed: Numbers.Cyclic.ZModulo from the standard library. This file was deprecated in 8.17 and has no known use cases. It is retained in the test suite to ensure consistency of CyclicAxioms (#17258, by Andres Erbsen).
Removed: ZArith.Zdigits in favor of Z.testbit (#18025, by Andres Erbsen).
Removed: long deprecated files in Arith: Div2.v, Even.v, Gt.v, Le.v, Lt.v, Max.v, Minus.v, Min.v, Mult.v, Plus.v, Arith_prebase.v (#18164, by Pierre Rousselin).
Deprecated: NArith.Ndigits and NArith.Ndist due to disuse. For most uses of Ndigits, N.testbit and similar functions seem more desirable. If you would like to continue using these files, please consider volunteering to maintain them, within stdlib or otherwise (#17732, by Andres Erbsen).
Deprecated: Strings.ByteVector in favor of Init.Byte (#18022, by Andres Erbsen).
Deprecated: Numbers.NaryFunctions due to disuse. If you are interested in continuting to use this module, please consider volunteering to maintain it, in stdlib or otherwise (#18026, by Andres Erbsen).
Added: Lemma cardinal_Add_In says that inserting an existing key with a new value doesn't change the size of a map, lemma Add_transpose_neqkey says that unequal keys can be inserted into a map in any order (#12096, by Isaac van Bakel and Jean-Christophe Léchenet).
Added: lemmas app_eq_cons, app_inj_pivot and rev_inj (#17787, by Stefan Haan, with help of Olivier Laurent).
Added: unfold_nth_error, nth_error_nil, nth_error_cons, nth_error_O, nth_error_S to Coq.Lists.List (#17998, by Jason Gross).
Added: Reflexive, Symmetric, Transitive, Antisymmetric, Asymmetric instances for Rle, Rge, Rlt, Rgt (#18059, by Jason Gross).

Extraction 

Fixed: In the error message about extraction of sort-polymorphic singleton inductive types, do not specifically refer to OCaml as other languages are also concerned (#17889, fixes #17817, by Hugo Herbelin).

Changes in 8.19.1

Kernel 

Fixed: incorrect abstraction of sort variables for opaque constants leading to an inconsistency (#18596 and #18630, fixes #18594, by Gaëtan Gilbert).
Fixed: memory corruption with vm_compute (rare but more likely with OCaml 5.1) (#18599, by Guillaume Melquiond).

Notations 

Changed: Found no matching notation to enable or disable is a warning instead of an error (#18670, by Pierre Roux).

Tactics 

Fixed: undeclared universe with multiple uses of abstract (#18640, fixes #18636, by Gaëtan Gilbert).

Ltac2 language 

Fixed: incorrect printing of constructor values with multiple arguments, and over-parenthesizing of constructor printing (#18560, fixes #18556, by Gaëtan Gilbert).
Fixed: incorrect declared type for Ltac2.FMap.fold (#18649, fixes #18635, by Gaëtan Gilbert).

Infrastructure and dependencies 

Fixed: missing conf- dependencies of the opam packages: coq-core depends on conf-linux-libc-dev when compiled on linux, and coq depends on conf-python-3 and conf-time to run the test suite (#18565, by Gaëtan Gilbert).
Fixed: avoid comitting symlinks to git which caused build failures on some Windows setups (#18550, fixes #18548, by Gaëtan Gilbert).

Changes in 8.19.2

Specification language, type inference 

Fixed: Regression from Coq 8.18 in the presence of a defined field in a primitive Record (#19088, fixes #19082, by Hugo Herbelin).

Notations 

Fixed: Printer sometimes failing to use a prefix or infix custom notation whose right-hand side refers to a different custom entry (#18089, fixes #18914, by Hugo Herbelin).

Tactics 

Fixed: abstract failing in the presence of admitted goals in the surrounding proof (#18945, fixes #18942, by Gaëtan Gilbert).

Ltac2 language 

Fixed: anomalies when using Ltac2 in VsCoq due to incorrect state handling of Ltac2 notations (#19096, fixes coq-community/vscoq#772, by Gaëtan Gilbert)

Commands and options 

Fixed: anomaly when using Include on a module containing a record declared with Primitive Projections (#18772, fixes #18769, by Jan-Oliver Kaiser)
Fixed: anomaly from Fixpoint with no arguments (#18741, by Hugo Herbelin)

CoqIDE 

Fixed: Position error/warning tooltips correctly when multibyte UTF-8 characters are present (#19137, fixes #19136, by Jim Fehrle).

Infrastructure and dependencies 

Fixed: compatibility with OCaml versions where effect is a keyword (#18863, by Remy Seassau)
Added: Coq is now compatible with memprof-limits interruption methods. This means that Coq will be recompiled when the library is installed / removed from an OPAM switch. (#18906, fixes #17760, by Emilio Jesus Gallego Arias).

Version 8.18

Summary of changes

Coq version 8.18 integrates two soundness fixes to the Coq kernel along with a host of improvements. We highlight a few impactful changes:

the default locality of Hint and Instance commands was switched to export.

the universe unification algorithm can now delay the commitment to a sort (the algorithm used to pick Type). Thanks to this feature many Prop and SProp annotations can be now omitted.

Ltac2 supports array literals, maps and sets of primitive datatypes such as names (of constants, inductive types, etc) and fine-grained control over profiling.

The warning system offers new categories, enabling finer (de)activation of specific warnings. This should be particularly useful to handle deprecations.

Many new lemmas useful for teaching analysis with Coq are now part of the standard library about real numbers.

The #[deprecated] attribute can now be applied to definitions.

The 41 contributors to the 8.18 version are: Reynald Affeldt, Tanaka Akira, Matthieu Baty, Yves Bertot, Lasse Blaauwbroek, Ana Borges, Kate Deplaix, Ali Caglayan, Cyril Cohen, Maxime Dénès, Andrej Dudenhefner, Andres Erbsen, Jim Fehrle, Yannick Forster, Paolo G. Giarrusso, Gaëtan Gilbert, Jason Gross, Samuel Gruetter, Stefan Haan, Hugo Herbelin, Yoshihiro Imai, Emilio Jesús Gallego Arias, Olivier Laurent, Meven Lennon-Bertrand, Rodolphe Lepigre, Yishuai Li, Guillaume Melquiond, Karl Palmskog, Pierre-Marie Pédrot, Stefan Radziuk, Ramkumar Ramachandra, Pierre Rousselin, Pierre Roux, Julin Shaji, Kazuhiko Sakaguchi, Weng Shiwei, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi, Hao Yang, Théo Zimmermann.

We are very grateful to the Coq community for their help in creating 8.18 in the 6 months since the release of Coq 8.17.0. Maxime Dénès and Enrico Tassi were the release managers.

Sophia-Antipolis, September 2023,

Enrico Tassi for the Coq development team

Changes in 8.18.0

Kernel 

Changed: the bad-relevance warning is now an error by default (#17172, by Pierre-Marie Pédrot).
Fixed: the kernel now checks that case elimination of private inductive types (cf private(matching)) is not used outside their defining module. Previously this was only checked in elaboration and the check could be avoided through some tactics, breaking consistency in the presence of axioms which rely on the elimination restriction to be consistent (#17452, fixes #9608, by Gaëtan Gilbert).
Fixed: a bug enabling native_compute to yield arbitrary floating-point values (#17872, fixes #17871, by Guillaume Melquiond and Pierre Roux, bug found by Jason Gross).

Specification language, type inference 

Changed: enhance the universe unification algorithm, which is now able to delay the definition of a sort. This allows omitting some explicit Prop and SProp annotations when writing terms. Some minor backwards compatibility issues can arise in rare cases, which can be solved with more explicit sort annotations (#16903, by Pierre-Marie Pédrot).
Changed: match compilation for primitive record avoids producing an encoding overhead for matches that are equivalent to a primitive projection (#17008, by Gaëtan Gilbert).
Added: volatile casts term :> type which do not leave a trace in the elaborated term. They are used by Printing Match All Subterms to display otherwise hidden subterms of match constructs (#16992, fixes #16918, by Gaëtan Gilbert).
Added: when printing uninterpreted terms (for instance through Print Ltac on Ltac foo := exact some_term), extensions to the term language (for instance Solving existential variables using tactics) are now printed correctly instead of as holes (_) (#17221, by Gaëtan Gilbert).
Added: Support for the local, global and export locality attributes for the single "field" of definitional typeclasses when using the :> and :: syntaxes for coercion and substructures (#17754, fixes #17451, by Pierre Roux).
Added: a hook in the coercion mechanism to enable programming coercions in external metalanguages such as Ltac, Ltac2, Elpi or OCaml plugins (#17794, by Pierre Roux).
Fixed: canonical instance matching match terms (#17206, fixes #17079, by Gaëtan Gilbert).
Fixed: universe constraint inference in module subtyping can trigger constant unfoldings (#17305, fixes #17303, by Gaëtan Gilbert).

Notations 

Removed: The '[=' keyword. '[=' tokens in notation definitions should be replaced with the pair of tokens '[' '='. If compatibility with Coq < 8.18 is needed, replace [= in uses of the notation with an added space ([ =) (#16788, fixes #16785, by Pierre Roux).
Added: Support for Printing Parentheses in custom notations (#17117, by Hugo Herbelin).
Added: Improve printing of reverse coercions. When a term x is elaborated to x' through a reverse coercion, return the term reverse_coercion x' x that is convertible to x' but displayed x thanks to the coercion reverse_coercion (#17484, by Pierre Roux).
Fixed: Add support to parse a recursive pattern as a sequence of terms in a recursive notation even when this recursive pattern is used in position of binders; it was formerly raising an anomaly (#16937, fixes #12467, by Hugo Herbelin).
Fixed: Improved ability to print notations involving anonymous binders (#17050, by Hugo Herbelin).
Fixed: anomaly with notations abbreviating a local variable or record field name (#17217, fixes #14975, by Hugo Herbelin).
Fixed: Ensure in all cases that a parsing rule is declared when the only parsing flag is given (#17318, fixes #17316, by Hugo Herbelin).
Fixed: In Number Notation, "abstract after N" was applied when number >= N. Now it is applied when number > N (#17478, by Jim Fehrle).

Tactics 

Changed: in the fringe case where the with clause of a call to specialize depends on a variable bound in the type, the tactic will now fail instead of silently producing a shelved evar (#17322, by Pierre-Marie Pédrot).
Changed: extensions to the term syntax through generic arguments (typically ltac:(), ltac2:() or ltac2's $) produce errors when used in term patterns (for instance patterns used to filter hints) instead of being treated as holes (_) (#17352, by Gaëtan Gilbert).
Changed: the case tactic and its variants always generate a pattern-matching node, regardless of their argument. In particular, they are now guaranteed to generate as many goals as there are constructors in the inductive type. Previously, they used to reduce to the corresponding branch when the argument βι-normalized to a constructor, resulting in a single goal (#17541, by Pierre-Marie Pédrot).
Changed: injection continues working using sigma types when Eqdep_dec has not been required even if an equality scheme was found, instead of failing (#17670, by Gaëtan Gilbert).
Changed: the unification heuristics for implicit arguments of the case tactic. We unconditionally recommend using destruct instead, and even more so in case of incompatibility (#17564, by Pierre-Marie Pédrot).
Removed: the no-argument form of the instantiate tactic, deprecated since 8.16 (#16910, by Pierre-Marie Pédrot).
Removed: undocumented tactics hresolve_core and hget_evar (#17035, by Gaëtan Gilbert).
Deprecated: the elimtype and casetype tactics (#16904, by Pierre-Marie Pédrot).
Deprecated: revert dependent, which is a misleadingly named alias of generalize dependent (#17669, by Gaëtan Gilbert).
Fixed: The simpl tactic now respects the simpl never flag even when the subject function is referred to through another definition (#13448, fixes #13428, by Yves Bertot).
Fixed: unification is less sensitive to whether a subterm is an indirection through a defined existential variable or a direct term node. This results in less constant unfoldings in rare cases (#16960, by Gaëtan Gilbert).
Fixed: untypable proof states generated by setoid_rewrite, which may cause some backwards-incompatibilities (#17304, fixes #17295, by Lasse Blaauwbroek).
Fixed: intropatterns destructing a term whose type is a product cannot silently create shelved evars anymore. Instead, it fails with an unsolvable variable. This can be fixed in a backwards compatible way by using the e-variant of the parent tactic (#17564, by Pierre-Marie Pédrot).
Fixed: the field_simplify tactic, so that it no longer introduces side-conditions when working on a hypothesis (#17591, by Guillaume Melquiond).
Fixed: the tauto tactic and its variants now try to match types up to universe unification. This makes them compatible with universe-polymorphic code (#8905, fixes #4721 and #5351, by Pierre-Marie Pédrot).

Ltac2 language 

Added: Support for parsing Ltac2 array literals [| ... |] (#16859, fixes #13976, by Samuel Gruetter).
Added: Finite set and map APIs for identifier, string, int, constant, inductive and constructor keys (#17347, c.f. #16409, by Gaëtan Gilbert).
Added: Ltac2 preterm antiquotation $preterm: (#17359, fixes #13977, by Gaëtan Gilbert).
Added: Ltac Profiling also profiles Ltac2 tactics. Ltac2 also provides tactics start_profiling stop_profiling and show_profile for finer grained control (#17371, fixes #10111, by Gaëtan Gilbert).
Added: primitives to build and compare values in Ltac2.Init.cast (#17468, by Gaëtan Gilbert).
Added: It is possible to define 0-argument externals (#17475, by Gaëtan Gilbert).
Added: Ltac2 quotations ltac2val:(ltac2 tactic) in Ltac1 which produce Ltac1 values (as opposed to ltac2:() quotations which are only useful for their side effects) (#17575, by Gaëtan Gilbert).
Fixed: nested notations involving Term Antiquotations (#17232, fixes #15864, by Gaëtan Gilbert).
Fixed: Parsing level of by clause of Ltac2's assert (#17508, fixes #17491, by Samuel Gruetter).
Fixed: multi_match!, multi_match! goal and the underlying Ltac2.Pattern.multi_match0 and Ltac2.Pattern.multi_goal_match0 now preserve exceptions from backtracking after a branch succeeded instead of replacing them with Match_failure (e.g. multi_match! constr:(tt) with tt => () end; Control.zero Not_found now fails with Not_found instead of Match_failure) (#17597, fixes #17594, by Gaëtan Gilbert).

Commands and options 

Changed: the default locality of Hint and Instance commands was switched to export (#16258, by Pierre-Marie Pédrot).
Changed: warning non-primitive-record is now in category records instead of record. This was the only use of record but the plural version is also used by cannot-define-projection future-coercion-class-constructor and future-coercion-class-field. (#16989, by Gaëtan Gilbert).
Changed: Eval prints information about existential variables like Check (#17274, by Gaëtan Gilbert).
Changed: The names of deprecation warnings now depend on the version in which they were introduced, using their "since" field. This enables deprecation warnings to be selectively enabled, disabled, or treated as an error, according to the version number provided in the deprecated attribute (#17489, fixes #16287, by Pierre Roux, reviewed by Ali Caglayan, Théo Zimmermann and Gaëtan Gilbert).
Changed: warnings can now have multiple categories allowing for finer user control on which warning to enable, disable or treat as an error (#17585, by Gaëtan Gilbert).
Changed: Template polymorphic inductive types are not implicitly added to the Keep Equalities table anymore when defined. This may change the behavior of equality-related tactics on such types (#17718, by Pierre-Marie Pédrot).
Changed: Warnings and warnings now emit a warning when trying to enable an unknown warning (there is still no warning when disabling an unknown warning as this behavior is useful for compatibility, or when enabling an unknown warning through the command line -w as the warning may be in a yet to be loaded plugin) (#17747, by Gaëtan Gilbert).
Removed: the flag Apply With Renaming which was deprecated since 8.15 (#16909, by Pierre-Marie Pédrot).
Removed: the Typeclasses Filtered Unification flag, deprecated since 8.16 (#16911, by Pierre-Marie Pédrot).
Removed: program attribute is not accepted anymore with commands Add Relation, Add Parametric Relation, Add Setoid, Add Parametric Setoid, Add Morphism, Add Parametric Morphism, Declare Morphism. Previously, it was accepted but ignored (#17042, by Théo Zimmermann).
Removed: the Elaboration StrictProp Cumulativity and Cumulative SProp flags. These flags became counterproductive after the introduction of sort variables in unification (#17114, fixes #17108, by Pierre-Marie Pédrot).
Removed: The Add LoadPath, Add Rec LoadPath, Add ML Path, and Remove LoadPath commands have been removed following deprecation. Users are encouraged to use the existing mechanisms in coq_makefile or dune to configure workspaces of Coq theories (#17394, by Emilio Jesus Gallego Arias).
Deprecated: Export modifier for Set. Use attribute export instead (#17333, by Gaëtan Gilbert).
Deprecated: the nonuniform attribute, now subsumed by warnings with "-uniform-inheritance" (#17716, by Pierre Roux).
Deprecated: Using Qed with Let. End the proof with Defined and use clearbody instead to get the same behavior (#17544, by Gaëtan Gilbert).
Added: About now prints information when a constant or inductive is syntactically equal to another through module aliasing (#16796, by Gaëtan Gilbert).
Added: Final Obligation command (#16817, by Gaëtan Gilbert).
Added: The deprecated attribute is now supported for definition-like constructions (#16890, fixes #12266, by Maxime Dénès and Gaëtan Gilbert).
Added: attributes warnings and alias warning to set warnings locally for a command (#16902, fixes #15893, by Gaëtan Gilbert).
Added: flag Printing Unfolded Projection As Match (off by default) to be able to distinguish unfolded and folded primitive projections (#16994, by Gaëtan Gilbert).
Added: option -time-file, like time but outputting to a file (#17430, by Gaëtan Gilbert).
Added: Validate Proof runs the type checker on the current proof, complementary with Guarded which runs the guard checker (#17467, by Gaëtan Gilbert).
Added: clearbody for Let to clear the body of a let-in in an interactive proof without kernel enforcement. (This is the behavior that was previously provided by using Qed, which is now deprecated for Lets.) (#17544, by Gaëtan Gilbert).
Added: option -time-file, like time but outputting to a file (#17430, by Gaëtan Gilbert).
Fixed: universe monomorphic inductives and records do not ignore Universe Minimization ToSet (#17285, fixes #13927, by Gaëtan Gilbert).

Command-line tools 

Changed: Do not pass the -rectypes flag by default in coq_makefile when compiling OCaml code, since it is no longer required by Coq. To re-enable passing the flag, put CAMLFLAGS+=-rectypes in the local makefile, e.g., CoqMakefile.local (see CoqMakefile.local) (#17038, by Karl Palmskog with help from Gaëtan Gilbert).
Changed: disable inclusion of variable binders in coqdoc indexes by default, and provide a new coqdoc option --binder-index for including them (#17045, fixes #13155, by Karl Palmskog).
Added: coqdoc handles multiple links to the same source. For example when declaring an inductive type t all occurences of t itself and its elimination principles like t_ind point to its declaration (#17118, by Enrico Tassi).
Added: Command line options -require lib (replacing -load-vernac-object lib) and -require-from root lib respectively equivalent to vernacular commands Require lib and From root Require lib (#17364, by Hugo Herbelin).
Added: coqtimelog2html command-line tool used to render the timing files produced with -time (which is passed by coq_makefile when environment variable TIMING is defined) (#17411, by Gaëtan Gilbert).
Fixed: coq_makefile avoids generating a command containing all files to install in a make rule, which could surpass the maximum single argument size in some developments (#17697, fixes #17721, by Gaëtan Gilbert).

CoqIDE 

Changed: XML Protocol now sends (and expects) full Coq locations, including line and column information. This makes some IDE operations (such as UTF-8 decoding) more efficient. Clients of the XML protocol can just ignore the new fields if they are not useful for them (#17382, fixes #17023, by Emilio Jesus Gallego Arias).

Standard library 

Changed: implementation of Vector.nth to follow OCaml and compute strict subterms (#16731, fixes #16738, by Andrej Dudenhefner).
Changed: drop the unnecessary second assumption NoDup l' from set_diff_nodup in ListSet.v, with -compat 8.17 providing the old version of set_diff_nodup for compatibility (#16926, by Karl Palmskog with help from Traian Florin Şerbănuţă and Andres Erbsen).
Changed: Moved instances from DecidableClass to files that prove the relevant decidability facts: Bool, PeanoNat, and BinInt (#17021, by Andres Erbsen).
Changed: Hint Extern btauto.Algebra.bool locality from global to export (#17281, by Andres Erbsen).
Changed: xorb to a simpler definition (#17427, by Guillaume Melquiond).
Changed lemmas in Reals/RIneq.v
- completeness_weak renamed as upper_bound_thm,
- le_epsilon renamed as Rle_epsilon,
- Rplus_eq_R0 renamed as Rplus_eq_0,
- Req_EM_T renamed as Req_dec_T,
- Rinv_r_simpl_m renamed as Rmult_inv_r_id_m,
- Rinv_r_simpl_l renamed as Rmult_inv_r_id_l,
- Rinv_r_simpl_r renamed as Rmult_inv_m_id_r,
- tech_Rgt_minus renamed as Rgt_minus_pos,
- tech_Rplus renamed as Rplus_le_lt_0_neq_0,
- IZR_POS_xI modified with 2 instead of 1 + 1,
- IZR_POS_xO modified with 2 instead of 1 + 1,
- Rge_refl modified with >= instead of <=
(#17036, by Pierre Rousselin, reviewer Laurent Théry).
Removed: Datatypes.prod_curry, Datatypes.prod_uncurry, Datatypes.prodT_curry, Datatypes.prodT_uncurry, Combinators.prod_curry_uncurry, Combinators.prod_uncurry_curry, Bool.leb, Bool.leb_implb, List.skipn_none, Zdiv.Z_div_mod_eq, Zdiv.div_Zdiv, Zdiv.mod_Zmod, FloatOps.frexp, FloatOps.ldexp, FloatLemmas.frexp_spec, FloatLemmas.ldexp_spec, RList.Rlist, Rlist.cons, Rlist.nil, RList.Rlength, Rtrigo_calc.cos3PI4, Rtrigo_calc.sin3PI4, MSetRBT.filter_app after deprecation for at least two Coq versions (#16920, by Olivier Laurent).
Deprecated: List.app_nil_end, List.app_assoc_reverse, List.ass_app, List.app_ass (#16920, by Olivier Laurent).
Deprecated: Coq.Lists.List.Forall2_refl (Coq.Lists.List.Forall2_nil has the same type) (#17646, by Gaëtan Gilbert).
Deprecated: ZArith.Zdigits in favor of Z.testbit. If you are aware of a use case of this module and would be interested in a drop-in replacement, please comment on the PR with information about the context that would benefit from such functinality (#17733, by Andres Erbsen).
Deprecated: Deprecation warnings are now generated for Numbers.Cyclic.Int31.Cyclic31, NNumbers.Cyclic.Int31.Int31, and NNumbers.Cyclic.Int31.Ring31. These modules have been deprecated since Coq 8.10. The modules under Numbers.Cyclic.Int63 remain available (#17734, by Andres Erbsen).
Deprecated lemmas in Reals/RIneq.v

inser_trans_R, IZR_neq, double, double_var, Rinv_mult_simpl, Rle_Rinv, Rlt_Rminus, Rminus_eq_0, Rminus_gt_0_lt, Ropp_div, Ropp_minus_distr', Rplus_sqr_eq_0_l, sum_inequa_Rle_lt_depr, S_O_plus_INR_depr, single_z_r_R1_depr, tech_single_z_r_R1_depr,

(#17036, by Pierre Rousselin, reviewer Laurent Théry).
Added: lemmas L_inj, R_inj, L_R_neq, case_L_R, case_L_R' to Fin.v, and nil_spec, nth_append_L, nth_append_R, In_nth, nth_replace_eq, nth_replace_neq, replace_append_L, replace_append_R, append_const, map_append, map2_ext, append_inj, In_cons_iff, Forall_cons_iff, Forall_map, Forall_append, Forall_nth, Forall2_nth, Forall2_append, map_shiftin, fold_right_shiftin, In_shiftin, Forall_shiftin, rev_nil, rev_cons, rev_shiftin, rev_rev, map_rev, fold_left_rev_right, In_rev, Forall_rev to VectorSpec.v (#16765, closes #6459, by Andrej Dudenhefner).
Added: lemmas iter_swap_gen, iter_swap, iter_succ, iter_succ_r, iter_add, iter_ind, iter_rect, iter_invariant for Nat.iter (#17013, by Stefan Haan with help from Jason Gross).
Added: module Zbitwise with basic relationships between bitwise and arithmetic operations on integers (#17022, by Andres Erbsen).
Added: lemmas forallb_filter, forallb_filter_id, partition_as_filter, filter_length, filter_length_le and filter_length_forallb (#17027, by Stefan Haan with help from Olivier Laurent and Andres Erbsen).
Added: lemmas in Reals/RIneq.v:

eq_IZR_contrapositive, INR_0, INR_1, INR_archimed, INR_unbounded, IPR_2_xH, IPR_2_xI, IPR_2_xO, IPR_eq, IPR_ge_1, IPR_gt_0, IPR_IPR_2, IPR_le, IPR_lt, IPR_not_1, IPR_xH, IPR_xI, IPR_xO, le_IPR, lt_1_IPR, lt_IPR, minus_IPR, mult_IPR, not_1_IPR, not_IPR, plus_IPR, pow_IPR, Rdiv_0_l, Rdiv_0_r, Rdiv_1_l, Rdiv_1_r, Rdiv_def, Rdiv_diag_eq, Rdiv_diag, Rdiv_diag_uniq, Rdiv_eq_compat_l, Rdiv_eq_compat_r, Rdiv_eq_reg_l, Rdiv_eq_reg_r, Rdiv_mult_distr, Rdiv_mult_l_l, Rdiv_mult_l_r, Rdiv_mult_r_l, Rdiv_mult_r_r, Rdiv_neg_neg, Rdiv_neg_pos, Rdiv_opp_l, Rdiv_pos_cases, Rdiv_pos_neg, Rdiv_pos_pos, Rexists_between, Rge_gt_or_eq_dec, Rge_gt_or_eq, Rge_lt_dec, Rge_lt_dec, Rgt_le_dec, Rgt_minus_pos, Rgt_or_le, Rgt_or_not_gt, Rinv_0_lt_contravar, Rinv_eq_compat, Rinv_eq_reg, Rinv_lt_0_contravar, Rinv_neg, Rinv_pos, Rle_gt_dec, Rle_half_plus, Rle_lt_or_eq, Rle_or_gt, Rle_or_not_le, Rlt_0_2, Rlt_0_minus, Rlt_ge_dec, Rlt_half_plus, Rlt_minus_0, Rlt_or_ge, Rlt_or_not_lt, Rminus_def, Rminus_diag, Rminus_eq_compat_l, Rminus_eq_compat_r, Rminus_plus_distr, Rminus_plus_l_l, Rminus_plus_l_r, Rminus_plus_r_l, Rminus_plus_r_r, Rmult_div_assoc, Rmult_div_l, Rmult_div_r, Rmult_div_swap, Rmult_gt_reg_r, Rmult_inv_l, Rmult_inv_m_id_r, Rmult_inv_r, Rmult_inv_r_id_l, Rmult_inv_r_id_m, Rmult_inv_r_uniq, Rmult_neg_cases, Rmult_neg_neg, Rmult_neg_pos, Rmult_pos_cases, Rmult_pos_neg, Rmult_pos_pos, Ropp_div_distr_l, Ropp_eq_reg, Ropp_neg, Ropp_pos, Rplus_0_l_uniq, Rplus_eq_0, Rplus_ge_reg_r, Rplus_gt_reg_r, Rplus_minus_assoc, Rplus_minus_l, Rplus_minus_r, Rplus_minus_swap, Rplus_neg_lt, Rplus_neg_neg, Rplus_neg_npos, Rplus_nneg_ge, Rplus_nneg_nneg, Rplus_nneg_pos, Rplus_npos_le, Rplus_npos_neg, Rplus_npos_npos, Rplus_pos_gt, Rplus_pos_nneg, Rplus_pos_pos, Rsqr_def

lemmas in Reals/R_Ifp.v: Int_part_spec, Rplus_Int_part_frac_part, Int_part_frac_part_spec

(#17036, by Pierre Rousselin, reviewer Laurent Théry).
Added: lemmas concat_length, flat_map_length, flat_map_constant_length, list_power_length to Lists.List (#17082, by Stefan Haan with help from Olivier Laurent).

Infrastructure and dependencies 

Changed: Sphinx 4.5.0 or above is now required to build the reference manual, so now / can be used as a quick search shortcut and Esc as a shortcut to remove search highlighting (#17772, fixes #15778, by Ana Borges).

Extraction 

Fixed: Anomaly when extracting within a module or module type (#17344, fixes #10739, by Hugo Herbelin).

Version 8.17

Summary of changes

Coq version 8.17 integrates a soundness fix to the Coq kernel along with a few new features and a host of improvements to the Ltac2 language and libraries. We highlight some of the most impactful changes here:

Fixed a logical inconsistency due to vm_compute in presence of side-effects in the enviroment (e.g. using Back or Fail).

It is now possible to dynamically enable or disable notations.

Support multiple scopes in Arguments and Bind Scope.

The tactics chapter of the manual has many improvements in presentation and wording. The documented grammar is semi-automatically checked for consistency with the implementation.

Fixes to the auto and eauto tactics, to respect hint priorities and the documented use of simple apply. This is a potentially breaking change.

New Ltac2 APIs, deep pattern-matching with as clauses and handling of literals, support for record types and preterms.

Move from :> to :: syntax for declaring typeclass fields as instances, fixing a confusion with declaration of coercions.

Standard library improvements.

While Coq supports OCaml 5, users are likely to experience slowdowns ranging from +10% to +50% compared to OCaml 4. Moreover, the native_compute machinery is not available when Coq is compiled with OCaml 5. Therefore, OCaml 5 support should still be considered experimental and not production-ready.

See the Changes in 8.17.0 section below for the detailed list of changes, including potentially breaking changes marked with Changed. Coq's reference manual for 8.17, documentation of the 8.17 standard library and developer documentation of the 8.17 ML API are also available.

Ali Caglayan, Emilio Jesús Gallego Arias, Gaëtan Gilbert and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure.

Erik Martin-Dorel has maintained the Coq Docker images that are used in many Coq projects for continuous integration.

Maxime Dénès, Paolo G. Giarrusso, Huỳnh Trần Khanh, and Laurent Théry have maintained the VsCoq extension for VS Code.

The opam repository for Coq packages has been maintained by Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/.

The Coq Platform has been maintained by Michael Soegtrop, with help from Karl Palmskog, Pierre Roux, Enrico Tassi and Théo Zimmermann.

Our current maintainers are Yves Bertot, Frédéric Besson, Ana Borges, Ali Caglayan, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, Andres Erbsen, Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann. See the Coq Team face book page for more details.

The 45 contributors to the 8.17 version are: Reynald Affeldt, Tanaka Akira, Lasse Blaauwbroek, Stephan Boyer, Ali Caglayan, Cyril Cohen, Maxime Dénès, Andrej Dudenhefner, Andres Erbsen, František Farka, Jim Fehrle, Paolo G. Giarrusso, Gaëtan Gilbert, Jason Gross, Alban Gruin, Stefan Haan, Hugo Herbelin, Wolf Honore, Bodo Igler, Jerry James, Emilio Jesús Gallego Arias, Ralf Jung, Jan-Oliver Kaiser, Wojciech Karpiel, Chantal Keller, Thomas Klausner, Olivier Laurent, Yishuai Li, Guillaume Melquiond, Karl Palmskog, Sudha Parimala, Pierre-Marie Pédrot, Valentin Robert, Pierre Roux, Julin S, Dmitry Shachnev, Michael Soegtrop, Matthieu Sozeau, Naveen Srinivasan, Sergei Stepanenko, Karolina Surma, Enrico Tassi, Li-yao Xia and Théo Zimmermann.

The Coq community at large helped improve this new version via the GitHub issue and pull request system, the coq-club@inria.fr mailing list, the Discourse forum and the Coq Zulip chat.

Version 8.17's development spanned 5 months from the release of Coq 8.16.0. Théo Zimmermann is the release manager of Coq 8.17. This release is the result of 414 merged PRs, closing 105 issues.

Nantes, February 2023,

Matthieu Sozeau for the Coq development team

Changes in 8.17.0

Kernel 

Fixed: inconsistency linked to vm_compute. The fix removes a vulnerable cache, thus it may result in slowdowns when vm_compute is used repeatedly, if you encounter such slowdowns please report your use case (#16958, fixes #16957, by Gaëtan Gilbert).
Fixed: Unexpected anomaly when checking termination of fixpoints containing match expressions with inaccessible branches (#17116, fixes #17073, by Hugo Herbelin).

Specification language, type inference 

Changed: Unused variable warning triggers even when catching a single case. This warning used to be triggered only when the unused variable was catching at least two cases (#16135, by Pierre Roux).
Fixed: Pattern-matching clauses were possibly lost when matching over a constructor from a singleton inductive type in the presence of implicit coercions (#17138, fixes #17137, by Hugo Herbelin).
Fixed: Possible anomaly when using syntax term.(proj) with projections defined in sections (#17174, fixes #17173, by Hugo Herbelin).

Notations 

Changed: When multiple tokens match the beginning of a sequence of characters, the longest matching token not cutting a subsequence of contiguous letters in the middle is used. Previously, this was only the longest matching token. See lexical conventions for details and examples (#16322, fixes #4712, by Hugo Herbelin).
Added: Enable Notation and Disable Notation commands to enable or disable previously defined notations (#12324 and #16945, by Hugo Herbelin and Pierre Roux, extending previous work by Lionel Rieg, review by Jim Fehrle).
Added: Support for multiple scopes in the Arguments command (#16472, by Pierre Roux, review by Jim Fehrle, Hugo Herbelin and Enrico Tassi).
Added: Attributes add_top and add_bottom to bind multiple scopes through the Bind Scope command (#16472, by Pierre Roux, review by Jim Fehrle, Hugo Herbelin and Enrico Tassi).

Tactics 

Changed: Documentation in the tactics chapter to give the current correct syntax, consolidate tactic variants for each tactic into a single, unified description for each tactic and many wording improvements. With this change, following similar changes to other chapters in previous releases, the correctness of documented syntax is assured by semi-automated tooling in all chapters except SSReflect (#15015, #16498, and #16659, by Jim Fehrle, reviewed by Théo Zimmermann, with help from many others).
Changed: eauto respects priorities of Extern hints (#16289, fixes #5163 and #16282, by Andrej Dudenhefner).

Warning

Code that relies on eager evaluation of Extern hints with high assigned cost by eauto will change its performance profile or potentially break. To approximate prior behavior, set to zero the cost of Extern hints, which may solve the goal in one step.
Changed: less discrepancies between auto hint evaluation and simple apply, exact tactics (#16293, fixes #16062 and #16323, by Andrej Dudenhefner).

Warning

auto may solve more goals. As a result, non-monotone use of auto such as tac1; auto. tac2. may break. For backwards compatibility use explicit goal management.
Removed: absurd_hyp tactic, that was marked as obsolete 15 years ago. Use contradict instead (#16670, by Théo Zimmermann).
Removed: the undocumented progress_evars tactical (#16843, by Théo Zimmermann).
Deprecated: the default intuition_solver (see intuition) now outputs warning intuition-auto-with-star if it solves a goal with auto with * that was not solved with just auto. In a future version it will be changed to just auto. Use intuition tac locally or Ltac Tauto.intuition_solver ::= tac globally to silence the warning in a forward-compatible way with your choice of tactic tac (auto, auto with *, auto with your prefered databases, or any other tactic) (#16026, by Gaëtan Gilbert).
Deprecated: > clear modifier that could be used in some tactics like apply and rewrite but was never documented. Open an issue if you actually depend on this feature (#16407, by Théo Zimmermann).
Fixed: auto now properly updates local hypotheses after hint application (#16302, fixes #15814 and #6332, by Andrej Dudenhefner).
Fixed: Make the behavior of destruct ... using ... more powerful and more similar to destruct ... (#16605, by Lasse Blaauwbroek).
Fixed: typeclass inference sometimes caused remaining holes to fail to be detected (#16743, fixes #5239, by Gaëtan Gilbert).

Ltac language 

Changed: Ltac redefinitions (with ::=) now respect local (#16106, by Gaëtan Gilbert).
Changed: In match goal, match goal with hyp := body : typ |- _ is syntax sugar for match goal with hyp := [ body ] : typ |- _ i.e. it matches typ with the type of the hypothesis rather than matching the body as a cast term. This transformation used to be done with any kind of cast (e.g. VM cast <:) and is now done only for default casts : (#16764, by Gaëtan Gilbert).

Ltac2 language 

Changed: Ltac2.Bool notations are now in a module Ltac2.Bool.BoolNotations (exported by default), so that these notations can be imported separately (#16536, by Jason Gross).
Changed: Constr.in_context enforces that the constr passed to it is a type (#16547, fixes #16540, by Gaëtan Gilbert).
Changed: goal matching functions from Ltac2.Pattern (matches_goal, lazy_goal_match0, multi_goal_match0 and one_goal_match0) have changed types to support matching hypothesis bodies (#16655, by Gaëtan Gilbert).
Added: Deep pattern matching for Ltac2 (#16023, by Gaëtan Gilbert).
Added: patterns for Ltac2 matches: as, records and literal integers and strings (#16179, by Gaëtan Gilbert).
Added: APIs for working with strings: Message.to_string, String.concat, cat, equal, compare, is_empty (#16217, by Gaëtan Gilbert).
Added: Ltac2.Constr.Unsafe.liftn (#16413, by Jason Gross).
Added: Ltac2.Constr.Unsafe.closedn, Ltac2.Constr.Unsafe.is_closed, Ltac2.Constr.Unsafe.occur_between, Ltac2.Constr.Unsafe.occurn (#16414, by Jason Gross).
Added: Ltac2.List.equal (#16429, by Jason Gross).
Added: Print Ltac2, Print Ltac2 Signatures and Locate can now find Ltac2 definitions (#16466, fixes #16418 and #16415, by Gaëtan Gilbert).
Added: Ltac2.Array.for_all2 and Ltac2.Array.equal (#16535, by Jason Gross).
Added: Ltac2.Constant.equal, Ltac2.Constant.t, Ltac2.Constructor.equal, Ltac2.Constructor.t, Ltac2.Evar.equal, Ltac2.Evar.t, Ltac2.Float.equal, Ltac2.Float.t, Ltac2.Meta.equal, Ltac2.Meta.t, Ltac2.Proj.equal, Ltac2.Proj.t, Ltac2.Uint63.equal, Ltac2.Uint63.t, Ltac2.Char.equal, Ltac2.Char.compare, Ltac2.Constr.Unsafe.Case.equal (#16537, by Jason Gross).
Added: Ltac2.Option.equal (#16538, by Jason Gross).
Added: syntax for Ltac2 record update { foo with field := bar } (#16552, fixes #10117, by Gaëtan Gilbert).
Added: Ltac2 record expressions support punning, i.e. { foo; M.bar } is equivalent to { foo := foo; M.bar := bar } (#16556, by Gaëtan Gilbert).
Added: match! goal support for matching hypothesis bodies (#16655, fixes #12803, by Gaëtan Gilbert).
Added: quotation and syntax class for preterms (#16740, by Gaëtan Gilbert).

SSReflect 

Added: port the additions made to ssrfun.v and ssrbool.v in math-comp PR #872 and PR #874, namely definitions olift and pred_oapp as well as lemmas all_sig2_cond, compA, obindEapp, omapEbind, omapEapp, omap_comp, oapp_comp, olift_comp, ocan_comp, eqbLR, eqbRL, can_in_pcan, pcan_in_inj, in_inj_comp, can_in_comp, pcan_in_comp and ocan_in_comp (#16158, by Pierre Roux).

Commands and options 

Changed: commands which set tactic options (currently Firstorder Solver and Obligation Tactic, as well as any defined by third party plugins) now support export locality. Note that such commands using global without export or using no explicit locality outside sections apply their effects when any module containing it (recursively) is imported. This will change in a future version. (#15274, fixes #15072, by Gaëtan Gilbert).
Changed: Hint and Instance commands with no locality attribute are deprecated. Previous versions generated a warning, but this version generates an error by default. This includes all Hint commands described in Creating Hints, Hint Rewrite, and Instance. As mentioned in the error, please add an explicit locality to the hint command. The default was #[global], but we recommend using #[export] where possible (#16004, fixes #13394, by Ali Caglayan).
Changed: Transparent obligations generated by Program do not produce an implicit Hint Unfold anymore (#16340, by Pierre-Marie Pédrot).
Changed: Print Typeclasses replaces the undocumented Print TypeClasses command which displays the list of typeclasses (#16690, fixes #16686, by Ali Caglayan).
Changed: The -async-proofs-tac-j command line option now accepts the argument 0, which makes par block interpreted without spawning any new process (#16837, by Pierre-Marie Pédrot).
Removed: the Program Naming flag, which was introduced as an immediately deprecated option in Coq 8.16 (#16519, by Pierre-Marie Pédrot).
Removed: undocumented and broken Solve Obligation command (the Solve Obligations command is untouched) (#16842, by Théo Zimmermann).
Deprecated :> syntax, to declare fields of Typeclasses as instances, since it is now replaced by :: (see of_type_inst). This will allow, in a future release, making :> declare Implicit Coercions as it does in record definitions (#16230, fixes #16224, by Pierre Roux, reviewed by Ali Caglayan, Jim Fehrle, Gaëtan Gilbert and Pierre-Marie Pédrot).
Added: An improved description of Proof using and section variables (#16168, by Jim Fehrle).
Added: :: syntax (see of_type_inst) to declare fields of records as typeclass instances (#16230, fixes #16224, by Pierre Roux, reviewed by Ali Caglayan, Jim Fehrle, Gaëtan Gilbert and Pierre-Marie Pédrot).
Added: The Print Keywords command, which prints all the currently-defined parser keywords and tokens (#16438, fixes #16375, by Gaëtan Gilbert).
Added: Print Grammar can print arbitrary nonterminals or the whole grammar instead of a small adhoc list of nonterminals (#16440, by Gaëtan Gilbert).
Fixed: Fast Name Printing flag no longer causes variable name capture when displaying a goal (#16395, fixes #14141, by Wojciech Karpiel).
Fixed: vm_compute ignored the bytecode-compiler command line flag (#16931, fixes #16929, by Gaëtan Gilbert).
Fixed: The Proof Mode command now gives an error if the specified proof mode doesn't exist. The command was not previously documented (#16981, fixes #16602, by Jim Fehrle).
Fixed: Backtracking over grammar modifications from plugins (such as added commands) (#17069, fixes #12575, by Gaëtan Gilbert).
Fixed: Anomaly instead of regular error on unsupported applied fix in Function (#17113, fixes #17110, by Hugo Herbelin).

Command-line tools 

Added: New documentation section Coq configuration basics covering use cases such as setting up Coq with opam, where/how to set up source code for your projects and use of _CoqProject (#15888, by Jim Fehrle).
Added: In _CoqProject files, expand paths that are directories to include appropriate files in (sub)directories (#16308, by Jim Fehrle).
Fixed: issues when using coq_makefile to build targets requiring both .vo and .glob files (typically documentation targets), where make would run multiple coqc processes on the same source file with racy behaviour (only fixed when using a make supporting "grouped targets" such as GNU Make 4.3) (#16757, by Gaëtan Gilbert).
Fixed: Properly process legacy attributes such as Global and Polymorphic in coqdoc to avoid omissions when using the -g (Gallina only) option (#17090, fixes #15933, by Karl Palmskog).

Standard library 

Changed: Class Saturate in ZifyCLasses.v, PRes now also takes operands (#16355, by František Farka on behalf of BedRock Systems, Inc.).
Changed: For uniformity of naming and ease of remembering, R_dist and theorems mentioning R_dist in their name become available with spelling Rdist (#16874, by Hugo Herbelin).
Removed: from Nat and N superfluous lemmas rs_rs', rs'_rs'', rbase, A'A_right, ls_ls', ls'_ls'', rs'_rs'', lbase, A'A_left, and also redundant non-negativity assumptions in gcd_unique, gcd_unique_alt, divide_gcd_iff, and gcd_mul_diag_l (#16203, by Andrej Dudenhefner).
Deprecated: notation _ ~= _ for JMeq in Coq.Program.Equality (#16436, by Gaëtan Gilbert).
Deprecated: lemma Finite_alt in FinFun.v, which is a weaker version of the newly added lemma Finite_dec (#16489, fixes #16479, by Bodo Igler, with help from Olivier Laurent).
Deprecated: Zmod, Zdiv_eucl_POS, Zmod_POS_bound, Zmod_pos_bound, and Zmod_neg_bound in ZArith.Zdiv (#16892, by Andres Erbsen).
Deprecated: Cyclic.ZModulo.ZModulo because there have been no known use cases for this module and because it does not implement Z/nZ for arbitrary n as one might expect based on the name. The same construction will remain a part of the Coq test suite to ensure consistency of CyclicAxioms (#16914, by Andres Erbsen).
Added: lemmas Permutation_incl_cons_inv_r, Permutation_pigeonhole, Permutation_pigeonhole_rel to Permutation.v, and Forall2_cons_iff, Forall2_length, Forall2_impl, Forall2_flip, Forall_Exists_exists_Forall2 to List.v (#15986, by Andrej Dudenhefner, with help from Dominique Larchey-Wendling and Olivier Laurent).
Added: modules Nat.Div0 and Nat.Lcm0 in PeanoNat, and N.Div0 and N.Lcm0 in BinNat containing lemmas regarding div and mod, which take into account n div 0 = 0 and n mod 0 = n. Strictly weaker lemmas are deprecated, and will be removed in the future. After the weaker lemmas are removed, the modules Div0 and Lcm0 will be deprecated, and their contents included directly into Nat and N. Locally, you can use Module Nat := Nat.Div0. or Module Nat := Nat.Lcm0. to approximate this inclusion (#16203, fixes #16186, by Andrej Dudenhefner).
Added: lemma measure_induction in Nat and N analogous to Wf_nat.induction_ltof1, which is compatible with the using clause for the induction tactic (#16203, by Andrej Dudenhefner).
Added: three lemmata related to finiteness and decidability of equality: Listing_decidable_eq, Finite_dec to FinFun.v and lemma NoDup_list_decidable to ListDec.v (#16489, fixes #16479, by Bodo Igler, with help from Olivier Laurent and Andrej Dudenhefner).
Added: lemma not_NoDup to ListDec.v and NoDup_app_remove_l, NoDup_app_remove_r to List.v (#16588, by Stefan Haan with a lot of help from Olivier Laurent and Ali Caglayan).
Added: the skipn_skipn lemma in Lists/List.v (#16632, by Stephan Boyer).
Added: lemmas nth_error_ext, map_repeat, rev_repeat to List.v, and to_list_nil_iff, to_list_inj to VectorSpec.v (#16756, by Stefan Haan).
Added: transparent extgcd to replace opaque euclid, euclid_rec, Euclid, and Euclid_intro in Znumtheory. Deprecated compatibility wrappers are provided (#16915, by Andres Erbsen).

Infrastructure and dependencies 

Changed: Coq is now built entirely using the Dune build system. Packagers and users that build Coq manually must use the new build instructions in the documentation (#15560, by Ali Caglayan, Emilio Jesus Gallego Arias, and Rudi Grinberg).
Changed: Coq is not compiled with OCaml's -rectypes option anymore. This means plugins which do not exploit it can also stop passing it to OCaml (#16007, by Gaëtan Gilbert).
Changed: Building Coq now requires Dune >= 2.9 (#16118, by Emilio Jesus Gallego Arias).
Changed: Coq Makefile targets pretty-timed, make-pretty-timed, make-pretty-timed-before, make-pretty-timed-after, print-pretty-timed, print-pretty-timed-diff, print-pretty-single-time-diff now generate more readable timing tables when absolute paths are used in _CoqProject / the arguments to coq_makefile, by stripping off the absolute prefix (#16268, by Jason Gross).
Changed: Coq's configure script now defaults to -native-compiler no. Previously, the default was -native-compiler ondemand, except on Windows. The behavior for users installing through opam does not change, i.e., it is -native-compiler no if the coq-native package is not installed, and -native-compiler yes otherwise (#16997, by Théo Zimmermann).
Removed: the -coqide switch to configure in Coq's build infrastructure (it stopped controlling what got compiled in the move to dune) (#16512, by Gaëtan Gilbert).
Removed: the -nomacintegration configure flag for CoqIDE. Now CoqIDE will always build with the proper platform-specific integration if available (#16531, by Emilio Jesus Gallego Arias).
Added: Coq now supports OCaml 5; note that OCaml 5 is not compatible with Coq's native reduction machine (#15494, #16925, #16947, #16959, #16988, #16991, #16996, #16997, #16999, #17010, and #17015 by Emilio Jesus Gallego Arias, Gaëtan Gilbert, Guillaume Melquiond, Pierre-Marie Pédrot, and others).
Added: OCaml 4.14 is now officially supported (#15867, by Gaëtan Gilbert).

Miscellaneous 

Changed: Module names are now added to the loadpath in alphabetical order for each (sub-)directory. Previously they were added in the order of the directory entries (as shown by "ls -U") (#16725, by Jim Fehrle).

Changes in 8.17.1

A variety of bug fixes and improvements to error messages, including:

Fixed: in some cases, coqdep emitted incorrect paths for META files which prevented dune builds for plugins from working correctly (#17270, fixes #16571, by Rodolphe Lepigre).
Fixed: Shadowing of record fields in extraction to OCaml (#17324, fixes #12813 and #14843 and #16677, by Hugo Herbelin).
Fixed: an impossible to turn off debug message "backtracking and redoing byextend on ..." (#17495, fixes #17488, by Gaëtan Gilbert).
Fixed: major memory regression affecting MathComp 2 (#17743, by Enrico Tassi and Pierre Roux).

Version 8.16

Summary of changes

Coq version 8.16 integrates changes to the Coq kernel and performance improvements along with a few new features. We highlight some of the most impactful changes here:

The guard checker (see Guarded) now ensures strong normalization under any reduction strategy.

Irrelevant terms (in the SProp sort) are now squashed to a dummy value during conversion, fixing a subject reduction issue and making proof conversion faster.

Introduction of reversible coercions, which allow coercions relying on meta-level resolution such as type-classes or canonical structures. Also allow coercions that do not fullfill the uniform inheritance condition.

Generalized rewriting support for rewriting with Type-valued relations and in Type contexts, using the Classes.CMorphisms library.

Added the boolean equality scheme command for decidable inductive types.

Added a Print Notation command.

Incompatibilities in name generation for Program obligations, eauto treatment of tactic failure levels, use of ident in notations, parsing of module expressions.

Standard library reorganization and deprecations.

Improve the treatment of standard library numbers by Extraction.

See the Changes in 8.16.0 section below for the detailed list of changes, including potentially breaking changes marked with Changed. Coq's reference manual for 8.16, documentation of the 8.16 standard library and developer documentation of the 8.16 ML API are also available.

Ali Caglayan, Emilio Jesús Gallego Arias, Gaëtan Gilbert and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure.

Erik Martin-Dorel has maintained the Coq Docker images that are used in many Coq projects for continuous integration.

The opam repository for Coq packages has been maintained by Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/.

The Coq Platform has been maintained by Michael Soegtrop, with help from Karl Palmskog, Enrico Tassi and Théo Zimmermann.

Our current maintainers are Yves Bertot, Frédéric Besson, Ana Borges, Ali Caglayan, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann. See the Coq Team face book page for more details.

The 57 contributors to the 8.16 versions are Tanaka Akira, Frédéric Besson, Martin Bodin, Ana Borges, Ali Caglayan, Minki Cho, Cyril Cohen, Juan Conejero, "stop-cran", Adrian Dapprich, Maxime Dénès, Stéphane Desarzens, Christian Doczkal, Andrej Dudenhefner, Andres Erbsen, Jim Fehrle, Emilio Jesús Gallego Arias, Attila Gáspár, Paolo G. Giarrusso, Gaëtan Gilbert, Rudi Grinberg, Jason Gross, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Bart Jacobs, Pierre Jouvelot, Ralf Jung, Grant Jurgensen, Jan-Oliver Kaiser, Wojciech Karpiel, Thomas Klausner, Ethan Kuefner, Fabian Kunze, Olivier Laurent, Yishuai Li, Erik Martin-Dorel, Guillaume Melquiond, Jean-Francois Monin, Pierre-Marie Pédrot, Rudy Peterson, Clément Pit-Claudel, Seth Poulsen, Ramkumar Ramachandra, Pierre Roux, Takafumi Saikawa, Kazuhiko Sakaguchi, Gabriel Scherer, Vincent Semeria, Kartik Singhal, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann.

The Coq community at large helped improve this new version via the GitHub issue and pull request system, the coq-club@inria.fr mailing list, the Discourse forum and the Coq Zulip chat.

Version 8.16's development spanned 6 months from the release of Coq 8.15.0. Pierre-Marie Pédrot is the release manager of Coq 8.16. This release is the result of 356 merged PRs, closing 99 issues.

Nantes, June 2022,

Matthieu Sozeau for the Coq development team

Changes in 8.16.0

Kernel 

Changed: Fixpoints are now expected to be guarded even in subterms erasable by reduction, thus getting rid of an artificial obstacle preventing to lift the assumption of weak normalization of Coq to an assumption of strong normalization; for instance (barring implementation bugs) termination of the type-checking algorithm of Coq is now restored (of course, as usual, up to the assumption of the consistency of set theory and type theory, i.e., equivalently, up to the weak normalization of type theory, a "physical" assumption, which has not been contradicted for decades and which specialists commonly believe to be a truth) (#15434, incidentally fixes the complexity issue #5702, by Hugo Herbelin).
Changed: Flag Unset Guard Checking nevertheless requires fixpoints to have an argument marked as decreasing in a type which is inductive (#15668, fixes #15621, by Hugo Herbelin).
Removed: Template polymorphism is now forbidden for mutual inductive types (#15965, by Gaëtan Gilbert).
Fixed: Inlining of non-logical objects (notations, hints, ...) was missing when applying a functor returning one of its arguments as e.g. in Module F (E:T) := E (#15412, fixes #15403, by Hugo Herbelin).
Fixed: We introduce a new irrelevant term in the reduction machine. It is used to shortcut computation of terms living in a strict proposition, and behaves as an exception. This restores subject reduction, and also makes conversion of large terms in SProp cheap (#15575, fixes #14015, by Pierre-Marie Pédrot).
Fixed: performance blowups while inferring variance information for Cumulative, NonCumulative inductive types (#15662, fixes #11741, by Gaëtan Gilbert).

Specification language, type inference 

Added: New clause as ident to the Record command to specify the name of the main argument to use by default in the type of projections (#14563, by Hugo Herbelin).
Added: Reversible coercions are coercions which cannot be represented by a regular coercion (a Gallina function) but rather a meta procedure, such as type class inference or canonical structure resolution (#15693, by Cyril Cohen, Pierre Roux, Enrico Tassi, reviewed by Ali Caglayan, Jim Fehrle and Gaëtan Gilbert).
Added: support for coercions not fulfilling the uniform inheritance condition, allowing more freedom for the parameters that are now inferred using unification, canonical structures or typeclasses (#15789, fixes #2828, #4593, #3115, #5222, #9696 and #8540, by Pierre Roux, reviewed by Ali Caglayan, Enrico Tassi, Kazuhiko Sakaguchi and Jim Fehrle).
Fixed: interpretation of {struct} fixpoint annotations when the principal argument comes from an implicit generalization (#15581, fixes #13157, by Gaëtan Gilbert).

Notations 

Removed: _ in ident entries in notations, which was deprecated in favor of name in 8.13. When you see messages like
```
Error: Notation "[ rel _ _ : _ | _ ]" is already defined at level 0
with arguments name, name, constr, constr while it is now required to be
at level 0 with arguments ident, ident, constr, constr.
```
replace ident with name in the Notation command. To ease the change, you can fix the deprecated-ident-entry warnings in Coq 8.15 (or 8.14 or 8.13). The warning can be turned into an error with -arg -w -arg +deprecated-ident-entry in the _CoqProject file (#15754, by Pierre Roux).
Added: When defining a recursive notation referring to another recursive notation, expressions of the form x .. y can be used where a sequence of binders is expected (#15291, grants #7911, by Hugo Herbelin).
Fixed: Coercions are disabled when typechecking parsers and printers of Number Notation (#15884, fixes #15843, by Pierre Roux).

Tactics 

Changed: The RewriteRelation type class is now used to declare relations inferable by the setoid_rewrite tactic to construct Proper instances. This can break developments that relied on existing Reflexive instances to infer relations. The fix is to simply add a (backwards compatible) RewriteRelation declaration for the relation. This change allows to set stricter modes on the relation type classes Reflexive, Symmetric, etc. (#13969, fixes #7916, by Matthieu Sozeau).
Changed: The setoid_rewrite tactic can now properly recognize homogeneous relations applied to types in different universes (#14138, fixes #13618, by Matthieu Sozeau).
Changed: The eauto tactic does not propagate internal Ltac failures with level > 0 anymore. Any failure caused by a hint now behaves as if it were a level 0 error (#15215, fixes #15214, by Pierre-Marie Pédrot).
Changed: rewrite when used to rewrite in multiple hypotheses (eg rewrite foo in H,H') requires that the term (foo) does not depend on the hypotheses it rewrites. When using rewrite in *, this means we only rewrite in hypotheses which do not appear in the term (#15426, fixes #3051 and #15448, by Gaëtan Gilbert).
Changed: When it fails, assert_succeeds fails with the argument tactic's original error instead of Tactic failure: <tactic closure> fails. (#15728, fixes #10970, by Gaëtan Gilbert).
Deprecated: the instantiate tactic without arguments. Since the move to the monadic tactic engine in 8.5, it was behaving as the identity (#15277, by Pierre-Marie Pédrot).
Added: generalized rewriting now supports rewriting with (possibly polymorphic) relations valued in Type. Use Classes.CMorphisms instead of Classes.Morphisms to declare Proper instances for rewrite (or setoid_rewrite) to use when rewriting with Type valued relations (#14137, fixes #4632, #5384, #5521, #6278, #7675, #8739, #11011, #12240, and #15279, by Matthieu Sozeau helped by Ali Caglayan).
Added: Tactics to obtain a micromega cone expression (aka witness) from an already reified goal. Using those tactics, the user can develop their own micromega tactics for their own types, using their own parsers (#15921, by Pierre Roux, reviewed by Frédéric Besson and Jim Fehrle).
Fixed: typeclasses eauto used with multiple hint databases respects priority differences for hints from separate databases (#15289, fixes #5304, by Gaëtan Gilbert).
Fixed: cbn has better support for combining simpl nomatch, ! and / specifiers (c.f. Arguments) (#15657, fixes #3989 and #15206, by Gaëtan Gilbert).

Tactic language 

Changed: Ltac match does not fail when the term to match contains an unfolded primitive projection (#15559, fixes #15554, by Gaëtan Gilbert).
Added: Ltac2 understands toplevel_selector and obeys Default Goal Selector. Note that par: is buggy when combined with abstract. Unlike Ltac1 even par: abstract tac is not properly treated (#15378, by Gaëtan Gilbert).
Added: Ltac2 Int functions div, mod, asr, lsl, lsr, land, lor , lxor and lnot (#15637, by Michael Soegtrop).
Fixed: Ltac2 apply and eapply not unifying with implicit arguments; unification inconsistent with exact and eexact (#15741, by Ramkumar Ramachandra).

SSReflect 

Fixed: have, suff and wlog support goals in SProp (#15121, by Enrico Tassi).

Commands and options 

Changed: Module now only allows parentheses around module arguments. For instance, Module M := (F X). is now a parsing error (#15355, by Gaëtan Gilbert).
Changed: Fail no longer catches anomalies, which it has done since Coq version 8.11. Now it only catches user errors (#15366, by Hugo Herbelin).
Changed: Program Definition in universe monomorphic mode does not accept non-extensible universe declarations (#15424, fixes #15410, by Gaëtan Gilbert).
Changed: The algorithm for name generation of anonymous variables for Program subproofs is now the same as the one used in the general case. This can create incompatibilities in scripts relying on such autogenerated names. The old scheme can be reactivated using the deprecated flag Program Naming (#15442, by Pierre-Marie Pédrot).
Removed: Universal Lemma Under Conjunction flag, that was deprecated in 8.15 (#15268, by Théo Zimmermann).
Removed: Abort no longer takes an ident as an argument (it has been ignored since 8.5) (#15669, by Gaëtan Gilbert).
Removed: Simplex flag, that was deprecated in 8.14. lia and lra will always use the simplex solver (that was already the default behaviour) (#15690, by Frédéric Besson).
Deprecated: Add LoadPath and Add Rec LoadPath. If this command is an important feature for you, please open an issue on GitHub <https://github.com/coq/coq/issues> and explain your workflow (#15652, by Gaëtan Gilbert).
Deprecated: the Typeclasses Filtered Unification flag. Due to a buggy implementation, it is unlikely this is used in the wild (#15752, by Pierre-Marie Pédrot).
Added: Scheme Boolean Equality command to generate the boolean equality for an inductive type whose equality is decidable. It is useful when Coq is able to generate the boolean equality but isn't powerful enough to prove the decidability of equality (unlike Scheme Equality, which tries to prove the decidability of the type) (#15526, by Hugo Herbelin).
Added: New more extensive algorithm based on the "parametricity" translation for canonically generating Boolean equalities associated to a decidable inductive type (#15527, by Hugo Herbelin).
Added: From … Dependency command to declare a dependency of a .v file on an external file. The coqdep tool generates build dependencies accordingly (#15650, fixes #15600, by Enrico Tassi).
Added: Print Notation command that prints the level and associativity of a given notation definition string (#15683, fixes #14907 and #4436 and #7730, by Ali Caglayan and Ana Borges, with help from Emilio Jesus Gallego Arias).
Added: a warning when trying to deprecate a definition (#15760, by Pierre Roux).
Added: A deprecation warning that the Class > syntax, which currently does nothing, will in the future declare coercions as it does when used in Record commands (#15802, by Pierre Roux, reviewed by Gaëtan Gilbert, Ali Caglayan, Jason Gross, Jim Fehrle and Théo Zimmermann).
Added: the nonuniform boolean attribute that silences the non-uniform-inheritance warning when user needs to declare such a coercion on purpose (#15853, by Pierre Roux, reviewed by Gaëtan Gilbert and Jim Fehrle).
Added: All commands which can import modules (e.g. Module Import M., Module F (Import X : T)., Require Import M., etc) now support import_categories. Require Import and Require Export also support filtered_import (#15945, fixes #14872, by Gaëtan Gilbert).
Fixed: Make Require Import M. equivalent to Require M. Import M. (#15347, fixes #3556, by Maxime Dénès).

Command-line tools 

Added: coq_makefile variable COQPLUGININSTALL to configure the installation of ML plugins (#15788, by Cyril Cohen and Enrico Tassi).
Added: Added -bytecode-compiler yesno flag for coqchk enabling vm_compute during checks, which is off by default (#15886, by Ali Caglayan).
Fixed: coqdoc confused by the presence of command Load in a file (#15511, fixes #15497, by Hugo Herbelin).

CoqIDE 

Added: Documentation of editing failed async mode proofs, how to configure key bindings and various previously undocumented details (#16070, by Jim Fehrle).

Standard library 

Changed: the signature scope of Classes.CMorphisms into signatureT (#15446, by Olivier Laurent).
Changed: the locality of typeclass instances Permutation_app' and Permutation_cons from global to export (#15597, fixes #15596, by Gaëtan Gilbert).
Removed: Int63, which was deprecated in favor of Uint63 in 8.14 (#15754, by Pierre Roux).
Deprecated: some obsolete files from the Arith part of the standard library (Div2, Even, Gt, Le, Lt, Max, Min, Minus, Mult, NPeano, Plus). Import Arith_base instead of these files. References to items in the deprecated files should be replaced with references to PeanoNat.Nat as suggested by the warning messages. Concerning the definitions of parity properties (even and odd), it is recommended to use Nat.Even and Nat.Odd. If an inductive definition of parity is required, the mutually inductive Nat.Even_alt and Nat.Odd_alt can be used. However, induction principles for Nat.Odd and Nat.Even are available as Nat.Even_Odd_ind and Nat.Odd_Even_ind. The equivalence between the non-inductive and mutually inductive definitions of parity can be found in Nat.Even_alt_Even and Nat.Odd_alt_Odd. All Hint declarations in the arith database have been moved to Arith_prebase and Arith_base. To use the results about Peano arithmetic, we recommend importing PeanoNat (or Arith_base to base it on the arith hint database) and using the Nat module. Arith_prebase has been introduced temporarily to ensure compatibility, but it will be removed at the end of the deprecation phase, e.g. in 8.18. Its use is thus discouraged (#14736, #15411, by Olivier Laurent, with help of Karl Palmskog).
Deprecated: identity inductive (replaced by the equivalent eq). Init.Logic_Type is removed (the only remaining definition notT is moved to Init.Logic) (#15256, by Olivier Laurent).
Deprecated: P_Rmin: use more general Rmin_case instead (#15388, fixes #15382, by Olivier Laurent).
Added: lemma count_occ_rev (#15397, by Olivier Laurent).
Added: Nat.EvenT and Nat.OddT (almost the same as Nat.Even and Nat.Odd but with output in Type. Decidability of parity (with output Type) is provided EvenT_OddT_dec as well as induction principles Nat.EvenT_OddT_rect and Nat.OddT_EvenT_rect (with output Type) (#15427, by Olivier Laurent).
Added: Added a proof of sin x < x for positive x and x < sin x for negative x (#15599, by stop-cran).
Added: decidability typeclass instances for Z.le, Z.lt, Z.ge and Z.gt, added lemmas Z.geb_ge and Z.gtb_gt (#15620, by Michael Soegtrop).
Added: lemmas Rinv_inv, Rinv_mult, Rinv_opp, Rinv_div, Rdiv_opp_r, Rsqr_div', Rsqr_inv', sqrt_inv, Rabs_inv, pow_inv, powerRZ_inv', powerRZ_neg', powerRZ_mult, cv_infty_cv_0, which are variants of existing lemmas, but without any hypothesis (#15644, by Guillaume Melquiond).
Added: a Leibniz equality test for primitive floats (#15719, by Pierre Roux, reviewed by Guillaume Melquiond).
Added: support for primitive floats in Scheme Boolean Equality (#15719, by Pierre Roux, reviewed by Hugo Herbelin).
Added: lemma le_add_l to NAddOrder.v. Use Nat.le_add_l as replacement for the deprecated Plus.le_plus_r (#16184, by Andrej Dudenhefner).

Infrastructure and dependencies 

Changed: Bumped lablgtk3 lower bound to 3.1.2 (#15947, by Pierre-Marie Pédrot).
Changed: Load plugins using findlib. This requires projects built with coq_makefile to either provide a hand written META file or use the -generate-meta-for-package option when applicable. As a consequence Declare ML Module now uses plugin names according to findlib, e.g. coq-aac-tactics.plugin. coqdep accepts -m META and uses the file to resolve plugin names to actual file names (#15220, fixes #7698, by Enrico Tassi).
Changed: Minimum supported zarith version is now 1.11 (#15483 and #16005 and #16030, closes #15496, by Gaëtan Gilbert and Théo Zimmermann and Jason Gross).
Changed: Bump the minimum OCaml version to 4.09.0. As a consequence the minimum supported ocamlfind version is now 1.8.1 (#15947 and #16046, fixes #14260 and #16015, by Pierre-Marie Pédrot and Théo Zimmermann).

Extraction 

Changed: ExtrOCamlInt63 no longer extracts comparison to int in OCaml; the extraction of Uint63.compare and Sint63.compare was also adapted accordingly (#15294, fixes #15280, by Li-yao Xia).
Changed: Extraction from nat to OCaml int uses Stdlib instead of Pervasives (#15333, by Rudy Nicolo Peterson).
Changed: The empty inductive type is now extracted to OCaml empty type available since OCaml 4.07 (#15967, by Pierre Roux).
Added: More extraction definitions for division and comparison of Z and N (#15098, by Li-yao Xia).
Fixed: Type int in files Number.v, Decimal.v and Hexadecimal.v have been renamed to signed_int (together with a compatibility alias int) so that they can be used in extraction without conflicting with OCaml's int type (#13460, fixes #7017 and #13288, by Hugo Herbelin).

Changes in 8.16.1

Kernel 

Fixed: conversion of Prod values in the native compiler (#16651, fixes #16645, by Pierre-Marie Pédrot).
Fixed: Coq 8.16.0 missed SProp check for opaque names in conversion (#16768, fixes #16752, by Hugo Herbelin).
Fixed: Pass the correct environment to compute η-expansion of cofixpoints in VM and native compilation (#16845, fixes #16831, by Pierre-Marie Pédrot).
Fixed: inconsistency with conversion of primitive arrays, and associated incomplete strong normalization of primitive arrays with lazy (#16850, fixes #16829, by Gaëtan Gilbert, reported by Maxime Buyse and Andres Erbsen).

Commands and options 

Fixed: Print Assumptions treats opaque definitions with missing proofs (as found in .vos files, see Compiled interfaces (produced using -vos)) as axioms instead of ignoring them (#16434, fixes #16411, by Gaëtan Gilbert).

CoqIDE 

Fixed: "Interrupt computations" now works correctly on Windows—except if you start CoqIDE as a background process, e.g. with coqide & in bash, in which case it won't work at all (#16142, fixes #13550, by Jim Fehrle).

Version 8.15

Summary of changes

Coq version 8.15 integrates many bug fixes, deprecations and cleanups as well as a few new features. We highlight some of the most impactful changes here:

The apply with tactic no longer renames arguments unless compatibility flag Apply With Renaming is set.

Improvements to the auto tactic family, fixing the Hint Unfold behavior, and generalizing the use of discrimination nets.

The typeclasses eauto tactic has a new best_effort option allowing it to return partial solutions to a proof search problem, depending on the mode declarations associated to each constraint. This mode is used by typeclass resolution during type inference to provide more precise error messages.

Many commands and options were deprecated or removed after deprecation and more consistently support locality attributes.

The Import command is extended with import_categories to select the components of a module to import or not, including features such as hints, coercions, and notations.

A visual Ltac debugger is now available in CoqIDE.

See the Changes in 8.15.0 section below for the detailed list of changes, including potentially breaking changes marked with Changed. Coq's reference manual for 8.15, documentation of the 8.15 standard library and developer documentation of the 8.15 ML API are also available.

Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure.

Erik Martin-Dorel has maintained the Coq Docker images that are used in many Coq projects for continuous integration.

The opam repository for Coq packages has been maintained by Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/.

The Coq Platform has been maintained by Michael Soegtrop and Enrico Tassi.

Our current maintainers are Yves Bertot, Frédéric Besson, Ali Caglayan, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann. See the Coq Team face book page for more details.

The 41 contributors to this version are Tanaka Akira, Frédéric Besson, Juan Conejero, Ali Caglayan, Cyril Cohen, Adrian Dapprich, Maxime Dénès, Stéphane Desarzens, Christian Doczkal, Andrej Dudenhefner, Jim Fehrle, Emilio Jesús Gallego Arias, Attila Gáspár, Gaëtan Gilbert, Jason Gross, Hugo Herbelin, Jasper Hugunin, Bart Jacobs, Ralf Jung, Grant Jurgensen, Jan-Oliver Kaiser, Wojciech Karpiel, Fabian Kunze, Olivier Laurent, Yishuai Li, Erik Martin-Dorel, Guillaume Melquiond, Jean-Francois Monin, Pierre-Marie Pédrot, Rudy Peterson, Clément Pit-Claudel, Seth Poulsen, Pierre Roux, Takafumi Saikawa, Kazuhiko Sakaguchi, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov and Théo Zimmerman.

The Coq community at large helped improve the design of this new version via the GitHub issue and pull request system, the Coq development mailing list coqdev@inria.fr, the coq-club@inria.fr mailing list, the Discourse forum and the Coq Zulip chat.

Version 8.15's development spanned 3 months from the release of Coq 8.14.0. Gaëtan Gilbert is the release manager of Coq 8.15. This release is the result of 384 merged PRs, closing 143 issues.

Nantes, January 2022,

Matthieu Sozeau for the Coq development team

Recent changes

Version 8.20

Summary of changes

Changes in 8.20.0

Version 8.19

Summary of changes

Changes in 8.19.0

Changes in 8.19.1

Changes in 8.19.2

Version 8.18

Summary of changes

Changes in 8.18.0

Version 8.17

Summary of changes

Changes in 8.17.0

Changes in 8.17.1

Version 8.16

Summary of changes

Changes in 8.16.0

Changes in 8.16.1

Version 8.15

Summary of changes

Changes in 8.15.0