diff --git a/master/refman/.doctrees/addendum/extraction.doctree b/master/refman/.doctrees/addendum/extraction.doctree
index 7288920f70..3a9999cdbc 100644
Binary files a/master/refman/.doctrees/addendum/extraction.doctree and b/master/refman/.doctrees/addendum/extraction.doctree differ
diff --git a/master/refman/.doctrees/addendum/generalized-rewriting.doctree b/master/refman/.doctrees/addendum/generalized-rewriting.doctree
index 6080010229..1c60824da0 100644
Binary files a/master/refman/.doctrees/addendum/generalized-rewriting.doctree and b/master/refman/.doctrees/addendum/generalized-rewriting.doctree differ
diff --git a/master/refman/.doctrees/addendum/program.doctree b/master/refman/.doctrees/addendum/program.doctree
index f6df4c5c7c..98051ed714 100644
Binary files a/master/refman/.doctrees/addendum/program.doctree and b/master/refman/.doctrees/addendum/program.doctree differ
diff --git a/master/refman/.doctrees/addendum/ring.doctree b/master/refman/.doctrees/addendum/ring.doctree
index 564cfd0fc4..4325a48950 100644
Binary files a/master/refman/.doctrees/addendum/ring.doctree and b/master/refman/.doctrees/addendum/ring.doctree differ
diff --git a/master/refman/.doctrees/addendum/universe-polymorphism.doctree b/master/refman/.doctrees/addendum/universe-polymorphism.doctree
index 7ca917259e..6064e38fd8 100644
Binary files a/master/refman/.doctrees/addendum/universe-polymorphism.doctree and b/master/refman/.doctrees/addendum/universe-polymorphism.doctree differ
diff --git a/master/refman/.doctrees/changes.doctree b/master/refman/.doctrees/changes.doctree
index 448fbfee3b..96cad99166 100644
Binary files a/master/refman/.doctrees/changes.doctree and b/master/refman/.doctrees/changes.doctree differ
diff --git a/master/refman/.doctrees/environment.pickle b/master/refman/.doctrees/environment.pickle
index 80e4771f60..bc62ef7a07 100644
Binary files a/master/refman/.doctrees/environment.pickle and b/master/refman/.doctrees/environment.pickle differ
diff --git a/master/refman/.doctrees/language/coq-library.doctree b/master/refman/.doctrees/language/coq-library.doctree
index 0839a808f2..8fe675acde 100644
Binary files a/master/refman/.doctrees/language/coq-library.doctree and b/master/refman/.doctrees/language/coq-library.doctree differ
diff --git a/master/refman/.doctrees/language/core/assumptions.doctree b/master/refman/.doctrees/language/core/assumptions.doctree
index 755dbdafcf..7264dbe3f9 100644
Binary files a/master/refman/.doctrees/language/core/assumptions.doctree and b/master/refman/.doctrees/language/core/assumptions.doctree differ
diff --git a/master/refman/.doctrees/language/core/basic.doctree b/master/refman/.doctrees/language/core/basic.doctree
index dd05fcd4fc..a9d59ae1a1 100644
Binary files a/master/refman/.doctrees/language/core/basic.doctree and b/master/refman/.doctrees/language/core/basic.doctree differ
diff --git a/master/refman/.doctrees/language/core/conversion.doctree b/master/refman/.doctrees/language/core/conversion.doctree
index 8e24ef1384..ba8f952eff 100644
Binary files a/master/refman/.doctrees/language/core/conversion.doctree and b/master/refman/.doctrees/language/core/conversion.doctree differ
diff --git a/master/refman/.doctrees/language/core/inductive.doctree b/master/refman/.doctrees/language/core/inductive.doctree
index 350ac70834..662b9ca4b5 100644
Binary files a/master/refman/.doctrees/language/core/inductive.doctree and b/master/refman/.doctrees/language/core/inductive.doctree differ
diff --git a/master/refman/.doctrees/language/core/modules.doctree b/master/refman/.doctrees/language/core/modules.doctree
index 6d025d5d2b..3551aba6c6 100644
Binary files a/master/refman/.doctrees/language/core/modules.doctree and b/master/refman/.doctrees/language/core/modules.doctree differ
diff --git a/master/refman/.doctrees/language/core/primitive.doctree b/master/refman/.doctrees/language/core/primitive.doctree
index 48981bd886..9b58dc4281 100644
Binary files a/master/refman/.doctrees/language/core/primitive.doctree and b/master/refman/.doctrees/language/core/primitive.doctree differ
diff --git a/master/refman/.doctrees/language/core/records.doctree b/master/refman/.doctrees/language/core/records.doctree
index a9c0191e62..59e241220b 100644
Binary files a/master/refman/.doctrees/language/core/records.doctree and b/master/refman/.doctrees/language/core/records.doctree differ
diff --git a/master/refman/.doctrees/language/extensions/arguments-command.doctree b/master/refman/.doctrees/language/extensions/arguments-command.doctree
index 4ee3ddd5a3..3e5b2cb001 100644
Binary files a/master/refman/.doctrees/language/extensions/arguments-command.doctree and b/master/refman/.doctrees/language/extensions/arguments-command.doctree differ
diff --git a/master/refman/.doctrees/language/extensions/canonical.doctree b/master/refman/.doctrees/language/extensions/canonical.doctree
index d641d3a0d0..0ce33d0c69 100644
Binary files a/master/refman/.doctrees/language/extensions/canonical.doctree and b/master/refman/.doctrees/language/extensions/canonical.doctree differ
diff --git a/master/refman/.doctrees/language/extensions/evars.doctree b/master/refman/.doctrees/language/extensions/evars.doctree
index 8d7d2b5d21..0b8be2ac9c 100644
Binary files a/master/refman/.doctrees/language/extensions/evars.doctree and b/master/refman/.doctrees/language/extensions/evars.doctree differ
diff --git a/master/refman/.doctrees/language/extensions/implicit-arguments.doctree b/master/refman/.doctrees/language/extensions/implicit-arguments.doctree
index 19aad7f4eb..b7b68e336e 100644
Binary files a/master/refman/.doctrees/language/extensions/implicit-arguments.doctree and b/master/refman/.doctrees/language/extensions/implicit-arguments.doctree differ
diff --git a/master/refman/.doctrees/language/extensions/match.doctree b/master/refman/.doctrees/language/extensions/match.doctree
index c05739d1e8..9145ed5ffb 100644
Binary files a/master/refman/.doctrees/language/extensions/match.doctree and b/master/refman/.doctrees/language/extensions/match.doctree differ
diff --git a/master/refman/.doctrees/proof-engine/ltac.doctree b/master/refman/.doctrees/proof-engine/ltac.doctree
index e02f04719d..cc92bb46f8 100644
Binary files a/master/refman/.doctrees/proof-engine/ltac.doctree and b/master/refman/.doctrees/proof-engine/ltac.doctree differ
diff --git a/master/refman/.doctrees/proof-engine/ltac2.doctree b/master/refman/.doctrees/proof-engine/ltac2.doctree
index 6f0a8f4371..5131c4187e 100644
Binary files a/master/refman/.doctrees/proof-engine/ltac2.doctree and b/master/refman/.doctrees/proof-engine/ltac2.doctree differ
diff --git a/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree b/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree
index a68ca395c7..ccda7ef9e6 100644
Binary files a/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree and b/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree differ
diff --git a/master/refman/.doctrees/proof-engine/tactics.doctree b/master/refman/.doctrees/proof-engine/tactics.doctree
index 88834999b3..e980746064 100644
Binary files a/master/refman/.doctrees/proof-engine/tactics.doctree and b/master/refman/.doctrees/proof-engine/tactics.doctree differ
diff --git a/master/refman/.doctrees/proof-engine/vernacular-commands.doctree b/master/refman/.doctrees/proof-engine/vernacular-commands.doctree
index fab0a552f4..3768dbc853 100644
Binary files a/master/refman/.doctrees/proof-engine/vernacular-commands.doctree and b/master/refman/.doctrees/proof-engine/vernacular-commands.doctree differ
diff --git a/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree b/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree
index af46d9b88c..98d6b31f86 100644
Binary files a/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree and b/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree differ
diff --git a/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree b/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree
index a6398aaca0..43719f6515 100644
Binary files a/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree and b/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree differ
diff --git a/master/refman/.doctrees/proofs/writing-proofs/equality.doctree b/master/refman/.doctrees/proofs/writing-proofs/equality.doctree
index 4bff550ff0..b4b741fa11 100644
Binary files a/master/refman/.doctrees/proofs/writing-proofs/equality.doctree and b/master/refman/.doctrees/proofs/writing-proofs/equality.doctree differ
diff --git a/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree b/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree
index 2142a40768..1813020110 100644
Binary files a/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree and b/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree differ
diff --git a/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree b/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree
index 42609fa84f..e10a16d7f8 100644
Binary files a/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree and b/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree differ
diff --git a/master/refman/.doctrees/user-extensions/syntax-extensions.doctree b/master/refman/.doctrees/user-extensions/syntax-extensions.doctree
index fe94786e4c..3841d42cff 100644
Binary files a/master/refman/.doctrees/user-extensions/syntax-extensions.doctree and b/master/refman/.doctrees/user-extensions/syntax-extensions.doctree differ
diff --git a/master/refman/.doctrees/using/libraries/funind.doctree b/master/refman/.doctrees/using/libraries/funind.doctree
index 68a97bdfca..09b3d98a9a 100644
Binary files a/master/refman/.doctrees/using/libraries/funind.doctree and b/master/refman/.doctrees/using/libraries/funind.doctree differ
diff --git a/master/refman/.doctrees/using/libraries/writing.doctree b/master/refman/.doctrees/using/libraries/writing.doctree
index 9c4aa86b00..38a958f751 100644
Binary files a/master/refman/.doctrees/using/libraries/writing.doctree and b/master/refman/.doctrees/using/libraries/writing.doctree differ
diff --git a/master/refman/_sources/changes.rst.txt b/master/refman/_sources/changes.rst.txt
index 9904e6a90c..9e85f2f541 100644
--- a/master/refman/_sources/changes.rst.txt
+++ b/master/refman/_sources/changes.rst.txt
@@ -14,7 +14,113 @@ Version 8.19
Summary of changes
~~~~~~~~~~~~~~~~~~
-TODO
+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:
+
+ - :ref:`sort-polymorphism` makes it possible to share common constructs
+ over `Type` `Prop` and `SProp`.
+
+ - The notation :g:`term%_scope` to set a scope only temporarily
+ (in addition to :g:`term%scope` for opening a
+ scope applying to all subterms).
+
+ - :tacn:`lazy`, :tacn:`simpl`, :tacn:`cbn` and :tacn:`cbv` and the associated :cmd:`Eval`
+ and :tacn:`eval` reductions learned to do head reduction when given flag `head`.
+
+ - :ref:`New Ltac2 APIs <819Ltac2>`, improved Ltac2 `exact` and
+ dynamic building of Ltac2 term patterns.
+
+ - New performance evaluation facilities: :cmd:`Instructions` to
+ count CPU instructions used by a command (Linux only) and
+ :ref:`profiling` system to produce trace files.
+
+ - New command :cmd:`Attributes` to assign attributes such as
+ :attr:`deprecated` to a library file.
+
+Notable breaking changes:
+
+ - :tacn:`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.
+
+ - :ref:`Removed old deprecated files <819Stdlib>` 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 Fixed:
Notations for applied constants equipped with multiple signatures of
@@ -1280,7 +1280,7 @@ Added:
When using Added:
In Changed:
recursive Deprecated:
The Changed:
Bump minimal Dune version required to build Coq to 3.6.1
@@ -1389,36 +1389,130 @@ TODO Coq version 8.19 extends the kernel universe polymorphism to
+polymorphism over sorts (e.g. We highlight some of the most impactful changes here: Sort polymorphism makes it possible to share common constructs
+over The notation New Ltac2 APIs, improved Ltac2 New performance evaluation facilities: New command Notable breaking changes: 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. Changed:
More informative message when a notation cannot be intepreted as a reference
@@ -1569,7 +1663,7 @@ Changed:
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
Unreleased changes¶
-
Kernel¶
+Kernel¶
Specification language, type inference¶
+Specification language, type inference¶
Notations¶
+Notations¶
Notations
Tactics¶
+Tactics¶
Z.to_euclidean_division_equations
, you can now pose
@@ -1311,7 +1311,7 @@ Tactics
Ltac language¶
+Ltac language¶
rewrite_strat
, rewstrategy
now supports the fixpoint operator fix ident := rewstrategy1
@@ -1326,7 +1326,7 @@ Ltac language
Ltac2 language¶
+Ltac2 language¶
let
and non mutable projections of syntactic values are considered syntactic values
@@ -1335,7 +1335,7 @@ Ltac2 language
-
SSReflect¶
+SSReflect¶
fun_scope
notation scope declared in ssrfun.v
is deprecated. Use
@@ -1345,7 +1345,7 @@ SSReflect
Commands and options¶
+Commands and options¶
Standard library¶
+Standard library¶
Infrastructure and dependencies¶
+Infrastructure and dependencies¶
Infrastructure and dependencies
Extraction¶
+Extraction¶
Miscellaneous¶
+Miscellaneous¶
Version 8.19¶
Summary of changes¶
-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.
+
+
+
+Type
Prop
and SProp
.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
.exact
and
+dynamic building of Ltac2 term patterns.Instructions
to
+count CPU instructions used by a command (Linux only) and
+Profiling system to produce trace files.Attributes
to assign attributes such as
+deprecated
to a library file.
+
+
+
+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.Changes in 8.19.0¶
-
Kernel¶
+Kernel¶
Notations¶
+Notations¶
Notations
Tactics¶
+Tactics¶
open_constr
in Ltac1 and Ltac2 does not perform evar normalization.
@@ -1605,6 +1699,12 @@ Tactics0 <= _ < _ 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,
@@ -1672,15 +1772,9 @@
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).
Fixed: Fix broken "r <num>" and "r <string>" commands in the coqtop Ltac debugger, which also affected the Proof General Ltac debugger @@ -1689,8 +1783,8 @@
Changed:
Array.empty
, Message.Format.stop
and Pattern.empty_context
are not thunked
@@ -1762,7 +1856,7 @@
Changed:
Let
with Qed
produces an opaque side definition
@@ -1820,7 +1914,7 @@
Changed:
Add a coqdep
option -w
to adjust warnings and allow turning then into
@@ -1841,8 +1935,8 @@
Changed:
reimplemented Ncring_tac
reification (used by nsatz
, cring
, but not ring
)
@@ -1900,7 +1994,7 @@
Fixed: In the error message about extraction of sort-polymorphic @@ -1959,21 +2053,21 @@
Removed:
The '[='
keyword. '[='
@@ -2093,7 +2187,7 @@
Changed:
in the fringe case where the with
clause of a call to specialize
@@ -2182,7 +2276,7 @@
Added:
Support for parsing Ltac2 array literals [| ... |]
@@ -2241,7 +2335,7 @@
Changed:
Do not pass the -rectypes
flag by default in
@@ -2426,7 +2520,7 @@
Changed: XML Protocol now sends (and expects) full Coq locations, including @@ -2439,7 +2533,7 @@
Changed:
implementation of Vector.nth
to follow OCaml and compute strict subterms
@@ -2701,7 +2795,7 @@
Changed: Sphinx 4.5.0 or above is now required to build the reference manual, so now / @@ -2713,7 +2807,7 @@
Fixed: Anomaly when extracting within a module or module type @@ -2735,18 +2829,18 @@
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.
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,
+
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.
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.
Changed:
Unused variable
warning
@@ -2855,8 +2949,8 @@
Changed: When multiple tokens match the beginning of a sequence of characters, @@ -2868,7 +2962,7 @@
Added: +
Added:
Enable Notation
and Disable Notation
commands
to enable or disable previously defined notations
(#12324 and #16945,
@@ -2886,8 +2980,8 @@
Changed:
Ltac
redefinitions (with ::=
) now respect local
@@ -2989,8 +3083,8 @@
Changed:
Ltac2.Bool
notations are now in a module Ltac2.Bool.BoolNotations
@@ -3074,8 +3168,8 @@
Added:
port the additions made to ssrfun.v
and ssrbool.v
in math-comp
@@ -3090,8 +3184,8 @@
Changed: commands which set tactic options (currently
Firstorder Solver
and Obligation Tactic
, as well as any
@@ -3196,8 +3290,8 @@
Added: New documentation section Coq configuration basics covering use cases such @@ -3226,8 +3320,8 @@
Changed:
Class Saturate
in ZifyCLasses.v
, PRes
now also takes operands
@@ -3316,8 +3410,8 @@
Changed: Coq is now built entirely using the Dune build system. Packagers and @@ -3383,8 +3477,8 @@
Changed: Module names are now added to the loadpath in @@ -3426,8 +3520,8 @@
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:
@@ -3447,7 +3541,7 @@Summary of changesname generation for Program obligations,
eauto
treatment of tactic failure levels, use ofident
in notations, parsing of module expressions.
Standard library reorganization and deprecations.
Standard library reorganization and deprecations.
Improve the treatment of standard library numbers by Extraction
.
Added:
New clause as ident
to the Record
command to specify
@@ -3611,8 +3705,8 @@
Changed:
The RewriteRelation
type class is now used to declare relations
@@ -3730,7 +3824,7 @@
Changed:
Ltac match
does not fail when the term to match contains an unfolded primitive projection
@@ -3753,8 +3847,8 @@
Added:
coq_makefile variable COQPLUGININSTALL
to configure the installation of ML plugins
@@ -3895,8 +3989,8 @@
Added: Documentation of editing failed async mode proofs, @@ -3906,11 +4000,11 @@
-
Changed:
the signature
scope of Classes.CMorphisms
into signatureT
(#15446,
@@ -3988,8 +4082,8 @@
Changed: Bumped lablgtk3 lower bound to 3.1.2 @@ -4023,11 +4117,11 @@
-
Changed:
ExtrOCamlInt63
no longer extracts comparison
to int
in OCaml;
the extraction of Uint63.compare
and Sint63.compare
was also adapted accordingly
@@ -4061,15 +4155,15 @@
Fixed: conversion of Prod values in the native compiler @@ -4095,8 +4189,8 @@
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
@@ -4105,8 +4199,8 @@
Fixed: "Interrupt computations" now works correctly on Windows—except @@ -4121,8 +4215,8 @@
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:
@@ -4193,24 +4287,24 @@Summary of changes
Changes in 8.15.0¶
---
- -
- -
- -
- -
- -
- -
- -
- -
- -
- -
- -
- +
+-- Kernel¶
++ -Kernel¶
Fixed: Name clash in a computation of the type of parameters of functorial @@ -4222,8 +4316,8 @@
Kernel -
Specification language, type inference¶
++ -Specification language, type inference¶
Changed:
Instance
warns about the default locality immediately rather than waiting until the instance is ready to be defined. @@ -4266,8 +4360,8 @@Specification language, type inference by Hugo Herbelin)
- Notations¶
++ -Notations¶
Changed: Terms printed in error messages may be more verbose if syntactic sugar would make it appear that the obtained and expected terms only differ in existential variables @@ -4319,8 +4413,8 @@
Notations
- Tactics¶
++ Tactics¶
@@ -4497,8 +4591,8 @@
Tactics
- Tactic language¶
++ Tactic language¶
Fixed: the parsing level of the Ltac2 tactic
now
@@ -4509,8 +4603,8 @@Tactic language -
SSReflect¶
++ -SSReflect¶
Changed: rewrite generates subgoals in the expected order (side conditions first, by @@ -4539,8 +4633,8 @@
SSReflect
- Commands and options¶
++ Commands and options¶
@@ -4640,8 +4734,8 @@
Commands and options -
Command-line tools¶
++ Command-line tools¶
Changed: Coqdoc options
--coqlib
and--coqlib_path
have been renamed @@ -4699,8 +4793,8 @@Command-line tools -
CoqIDE¶
++ CoqIDE¶
Changed: CoqIDE unicode keys for brackets (e.g.
langle
) now bind to unicode mathematical symbols rather than unicode CJK brackets @@ -4727,8 +4821,8 @@CoqIDE -
Standard library¶
++ Standard library¶
Changed: Permutation-related Proper instances are now at default priority instead of priority
10
@@ -4786,8 +4880,8 @@Standard library -
Infrastructure and dependencies¶
++ -Infrastructure and dependencies¶
Changed: Coq's continuous integration now provides a more accessible Windows @@ -4840,8 +4934,8 @@
Infrastructure and dependencies
- Extraction¶
++ Extraction¶
Changed: replaced
Big
module withBig_int_Z
functions fromzarith
.OCaml code extracted with the following modules should be linked to the @@ -4863,18 +4957,18 @@
Extraction
Changes in 8.15.1¶
-+-- Kernel¶
++ Kernel¶
Fixed: cases of incompletenesses in the guard condition for fixpoints in @@ -4889,8 +4983,8 @@
Kernel -
Notations¶
++ -Notations¶
Fixed: Check for prior declaration of a custom entry was missing for notations in only printing mode @@ -4899,8 +4993,8 @@
Notations
- Tactics¶
++ -Tactics¶
Fixed:
rewrite_strat
regression in 8.15.0 related toTransitive
instances @@ -4925,8 +5019,8 @@Tactics
- Command-line tools¶
++ Command-line tools¶
Fixed: a bug where
coqc -vok
was not creating an empty '.vok' file @@ -4934,8 +5028,8 @@Command-line tools -
CoqIDE¶
++ CoqIDE¶
Fixed: Line numbers shown in the Errors panel were incorrect; @@ -4959,8 +5053,8 @@
CoqIDE -
Miscellaneous¶
++ Miscellaneous¶
Fixed: Ensure that the names of arguments of inductive schemes are distinct @@ -4975,15 +5069,15 @@
Miscellaneous
Changes in 8.15.2¶
-+ -- Tactics¶
++ -Tactics¶
Added:
intuition
anddintuition
useTauto.intuition_solver
(defined asauto with *
) instead of hardcodingauto with *
. @@ -4998,8 +5092,8 @@Tactics
- CoqIDE¶
++ CoqIDE¶
Fixed: multiple CoqIDE bugs @@ -5017,8 +5111,8 @@
CoqIDE -
Standard library¶
++ Standard library¶
@@ -5110,25 +5204,25 @@
Fixed: an incorrect implementation of SFClassify, allowing for a proof of False since @@ -5032,8 +5126,8 @@
Standard library
Version 8.14¶
-- Summary of changes¶
++ Summary of changes¶
Coq version 8.14 integrates many usability improvements, as well as an important change in the core language. The main changes include:
@@ -5048,13 +5142,13 @@Summary of changes.vo file. It is supported by
coq_makefile
.- -
Improvements to typeclasses and canonical structure resolution, allowing more terms to be considered as classes or keys.
More control over notations declarations and support +
- -
More control over notations declarations and support for primitive types in string and number notations.
Removal of deprecated tactics, notably
omega
, which has +- -
Removal of deprecated tactics, notably
omega
, which has been replaced by a greatly improvedlia
, along with many bug fixes.New Ltac2 APIs for interaction with Ltac1, manipulation of +
- -
New Ltac2 APIs for interaction with Ltac1, manipulation of inductive types and printing.
Many changes and additions to the standard library in the numbers, +
Many changes and additions to the standard library in the numbers, vectors and lists libraries. A new signed primitive integers library
Sint63
is available in addition to the unsignedUint63
library.Summary of changes
Changes in 8.14.0¶
---
- -
- -
- -
- -
- -
- -
- -
- -
- -
- -
- -
- -
- +
+-- Kernel¶
++ Kernel¶
@@ -5159,8 +5253,8 @@
Kernel -
Specification language, type inference¶
++ -Specification language, type inference¶
@@ -5202,11 +5296,11 @@
Specification language, type inference by Hugo Herbelin).
- Notations¶
++ -Notations¶
-+
Changed: Flag
Printing Notations
no longer controls whether strings and numbers are printed raw @@ -5264,11 +5358,11 @@Notations
- Tactics¶
++ -Tactics¶
-- Tactic language¶
++ Tactic language¶
-+
Changed: Renamed Ltac2
Bool.eq
intoBool.equal
for uniformity. The old function is now a deprecated alias @@ -5457,8 +5551,8 @@Tactic language -
SSReflect¶
++ -SSReflect¶
Added: A test that the notations
{in _, _}
and{pred _}
fromssrbool.v
are displayed correctly @@ -5471,8 +5565,8 @@SSReflect
- Commands and options¶
++ Commands and options¶
Changed:
Hint Rewrite
now supports locality attributes (includingexport
) like other Hint commands @@ -5568,8 +5662,8 @@Commands and options -
Command-line tools¶
++ Command-line tools¶
Changed:
coqc
now enforces that at most a single.v
file can be passed in @@ -5613,7 +5707,7 @@Command-line tools -
Native Compilation¶
+Native Compilation¶
@@ -5638,11 +5732,11 @@
Native Compilation -
CoqIDE¶
++ -CoqIDE¶
-+
Added: Ltac debugger support in CoqIDE (see
Ltac Debug
). Debugger output and prompts appear in the Messages panel @@ -5653,11 +5747,11 @@CoqIDE -
Standard library¶
++ -Standard library¶
-+
Changed: Minor Changes to
Rpower
: Generalizesexp_ineq1
to hold for all non-zero numbers. @@ -5797,8 +5891,8 @@Standard library#14256, by Jason Gross).
- Infrastructure and dependencies¶
++ Infrastructure and dependencies¶
@@ -5845,8 +5939,8 @@
Infrastructure and dependencies
- Miscellaneous¶
++ Miscellaneous¶
Changed: The representation of micromega caches was slightly @@ -5866,8 +5960,8 @@
Miscellaneous
Changes in 8.14.1¶
-- Kernel¶
++ Kernel¶
Fixed: Fix the implementation of persistent arrays used by the VM and native compute @@ -5878,8 +5972,8 @@
Kernel -
Specification language, type inference¶
++ -Specification language, type inference¶
Fixed: Missing registration of universe constraints in
Module Type
elaboration @@ -5888,8 +5982,8 @@Specification language, type inference
- Tactics¶
++ Tactics¶
Fixed:
abstract
more robust with respect to Ltacconstr
bindings containing @@ -5904,8 +5998,8 @@Tactics -
Commands and options¶
++ Commands and options¶
Fixed: anomaly with
Extraction Conservative Types
when extracting @@ -5925,8 +6019,8 @@Commands and options
Version 8.13¶
-- Summary of changes¶
++ Summary of changes¶
Coq version 8.13 integrates many usability improvements, as well as extensions of the core language. The main changes include:
@@ -5952,11 +6046,11 @@Summary of changesrationale and guidelines for details.
- -
General support for boolean attributes.
Many improvements to the handling of notations, +
- -
Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior.
Tactic improvements in
lia
and itszify
preprocessing step, +Tactic improvements in
lia
and itszify
preprocessing step, now supporting reasoning on boolean operators such asZ.leb
and supporting primitive integersInt63
.- @@ -6015,23 +6109,23 @@
Typing flags can now be specified per-constant / inductive.
Summary of changes
Changes in 8.13+beta1¶
---
- -
- -
- -
- -
- -
- -
- -
- -
- -
- -
- +
+-- Kernel¶
++ Kernel¶
@@ -6070,8 +6164,8 @@
Kernel -
Specification language, type inference¶
++ -Specification language, type inference¶
@@ -6181,8 +6275,8 @@
Specification language, type inference
- Notations¶
++ -Notations¶
Changed: In notations (except in custom entries), the misleading
syntax_modifier
@@ -6303,8 +6397,8 @@Specification language, type inference
- Tactics¶
++ -Tactics¶
Changed: In
refine
, new existential variables unified with existing ones are no @@ -6378,8 +6472,8 @@Specification language, type inference by Hugo Herbelin).
- Tactic language¶
++ Tactic language¶
Added: An if-then-else syntax to Ltac2 @@ -6394,8 +6488,8 @@
Tactic language -
SSReflect¶
++ -SSReflect¶
Added: SSReflect intro pattern ltac views
/[dup]
,/[swap]
and/[apply]
@@ -6408,8 +6502,8 @@SSReflect
- Commands and options¶
++ -Commands and options¶
- CoqIDE¶
++ CoqIDE¶
Added: Support showing diffs for
Show Proof
in CoqIDE from theView
menu. @@ -6507,8 +6601,8 @@CoqIDE -
Standard library¶
++ Standard library¶
Changed: In the reals theory changed the epsilon in the definition of the modulus of convergence for CReal from 1/n (n in positive) to 2^z (z in Z) @@ -6567,8 +6661,8 @@
Standard library -
Infrastructure and dependencies¶
++ Infrastructure and dependencies¶
Changed: When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC @@ -6593,8 +6687,8 @@
Infrastructure and dependencies
Changes in 8.13.0