Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2024-07-01 11:21:23 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.18349 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Mon Jul 1 11:21:23 2024 rev:28 rq:1184115 version:8.19.2 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2024-03-08 18:09:15.458307812 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.18349/coq.changes 2024-07-01 11:22:05.982840538 +0200 @@ -1,0 +2,19 @@ +Sun Jun 30 17:20:06 UTC 2024 - Aaron Puchert <[email protected]> + +- Update to version 8.19.2. + * Fixed a regression from Coq 8.18 in the presence of a defined + field in a primitive `Record`. + * Fixed an issue where the printer was sometimes failing to use a + prefix or infix custom notation whose right-hand side refers to + a different custom entry. + * Fixed `abstract` failure in the presence of admitted goals in + the surrounding proof. + * Fixed issues when using Ltac2 in VsCoq due to incorrect state + handling of Ltac2 notations. + * Fixed `Include` on a module containing a record declared with + `Primitive Projections`. + * Fixed an issue in `Fixpoint` with no arguments. + * Position error/warning tooltips correctly when multibyte UTF-8 + characters are present. + +------------------------------------------------------------------- Old: ---- coq-8.19.1.tar.gz coq-refman-8.19.1.tar.xz coq-stdlib-8.19.1.tar.xz New: ---- coq-8.19.2.tar.gz coq-refman-8.19.2.tar.xz coq-stdlib-8.19.2.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.m5bbaR/_old 2024-07-01 11:22:06.718867351 +0200 +++ /var/tmp/diff_new_pack.m5bbaR/_new 2024-07-01 11:22:06.722867497 +0200 @@ -26,7 +26,7 @@ %endif Name: coq -Version: 8.19.1 +Version: 8.19.2 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only ++++++ coq-8.19.1.tar.gz -> coq-8.19.2.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.19.1.tar.gz /work/SRC/openSUSE:Factory/.coq.new.18349/coq-8.19.2.tar.gz differ: char 13, line 1 ++++++ coq-refman-8.19.1.tar.xz -> coq-refman-8.19.2.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.19.1.tar.xz /work/SRC/openSUSE:Factory/.coq.new.18349/coq-refman-8.19.2.tar.xz differ: char 13, line 1 ++++++ coq-stdlib-8.19.1.tar.xz -> coq-stdlib-8.19.2.tar.xz ++++++
