Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2020-12-14 18:09:33 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.2328 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Mon Dec 14 18:09:33 2020 rev:8 rq:855595 version:8.12.2 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2020-12-04 21:27:55.806076799 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.2328/coq.changes 2020-12-14 18:10:09.779687482 +0100 @@ -1,0 +2,9 @@ +Sun Dec 13 15:55:58 UTC 2020 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.12.2. Fixes two impacting 8.12 regressions: + * Fixed a regression causing notations mentioning a coercion to + be ignored. + * Fixed a regression causing incomplete inference of implicit + arguments in exists. + +------------------------------------------------------------------- Old: ---- coq-8.12.1.tar.gz New: ---- coq-8.12.2.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.Hm3aNr/_old 2020-12-14 18:10:10.635688332 +0100 +++ /var/tmp/diff_new_pack.Hm3aNr/_new 2020-12-14 18:10:10.639688337 +0100 @@ -18,7 +18,7 @@ Name: coq -Version: 8.12.1 +Version: 8.12.2 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only ++++++ coq-8.12.1.tar.gz -> coq-8.12.2.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.12.1.tar.gz /work/SRC/openSUSE:Factory/.coq.new.2328/coq-8.12.2.tar.gz differ: char 13, line 1 _______________________________________________ openSUSE Commits mailing list -- commit@lists.opensuse.org To unsubscribe, email commit-le...@lists.opensuse.org List Netiquette: https://en.opensuse.org/openSUSE:Mailing_list_netiquette List Archives: https://lists.opensuse.org/archives/list/commit@lists.opensuse.org
