Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2021-12-13 20:44:29 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.2520 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Mon Dec 13 20:44:29 2021 rev:14 rq:940115 version:8.14.1 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2021-10-21 23:55:40.468030058 +0200 +++ /work/SRC/openSUSE:Factory/.coq.new.2520/coq.changes 2021-12-13 20:50:32.988640810 +0100 @@ -1,0 +2,18 @@ +Sun Dec 12 20:11:15 UTC 2021 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.14.1. + * Fixed the implementation of persistent arrays used by the VM + and native compute so that it uses a uniform representation. + Previously, storing primitive floats inside primitive arrays + could cause memory corruption. + * Fixed missing registration of universe constraints in Module + Type elaboration. + * Made `abstract` more robust with respect to Ltac `constr` + bindings containing existential variables. + * Correct support of trailing `let` by tactic `specialize`. + * Fixed an anomaly with `Extraction Conservative Types` when + extracting pattern-matching on singleton types. + * Regular error instead of an anomaly when calling `Separate + Extraction` in a module. + +------------------------------------------------------------------- Old: ---- coq-8.14.0.tar.gz coq-refman-8.14.0.tar.xz coq-stdlib-8.14.0.tar.xz New: ---- coq-8.14.1.tar.gz coq-refman-8.14.1.tar.xz coq-stdlib-8.14.1.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.paB4Y9/_old 2021-12-13 20:50:33.480641124 +0100 +++ /var/tmp/diff_new_pack.paB4Y9/_new 2021-12-13 20:50:33.484641127 +0100 @@ -20,7 +20,7 @@ %bcond_without ide Name: coq -Version: 8.14.0 +Version: 8.14.1 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only ++++++ coq-8.14.0.tar.gz -> coq-8.14.1.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.14.0.tar.gz /work/SRC/openSUSE:Factory/.coq.new.2520/coq-8.14.1.tar.gz differ: char 28, line 1 ++++++ coq-refman-8.14.0.tar.xz -> coq-refman-8.14.1.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.14.0.tar.xz /work/SRC/openSUSE:Factory/.coq.new.2520/coq-refman-8.14.1.tar.xz differ: char 26, line 1 ++++++ coq-stdlib-8.14.0.tar.xz -> coq-stdlib-8.14.1.tar.xz ++++++
