Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2022-11-27 12:53:03 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.1597 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Sun Nov 27 12:53:03 2022 rev:19 rq:1038367 version:8.16.1 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2022-09-09 18:29:30.801265719 +0200 +++ /work/SRC/openSUSE:Factory/.coq.new.1597/coq.changes 2022-11-27 12:53:15.379286031 +0100 @@ -1,0 +2,15 @@ +Sat Nov 26 22:20:18 UTC 2022 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.16.1. + * Fixed the conversion of `Prod` values in the native compiler. + * Added `SProp` check for opaque names in conversion. + * Pass the correct environment to compute η-expansion of + cofixpoints in VM and native compilation. + * Fixed an inconsistency with conversion of primitive arrays, and + associated incomplete strong normalization of primitive arrays + with `lazy`. + * `Print Assumptions` treats opaque definitions with missing + proofs (as found in .vos files, produced using -vos) as axioms + instead of ignoring them. + +------------------------------------------------------------------- Old: ---- coq-8.16.0.tar.gz coq-refman-8.16.0.tar.xz coq-stdlib-8.16.0.tar.xz New: ---- coq-8.16.1.tar.gz coq-refman-8.16.1.tar.xz coq-stdlib-8.16.1.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.0lx9CL/_old 2022-11-27 12:53:16.243291044 +0100 +++ /var/tmp/diff_new_pack.0lx9CL/_new 2022-11-27 12:53:16.247291067 +0100 @@ -20,7 +20,7 @@ %bcond_without ide Name: coq -Version: 8.16.0 +Version: 8.16.1 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only ++++++ coq-8.16.0.tar.gz -> coq-8.16.1.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.16.0.tar.gz /work/SRC/openSUSE:Factory/.coq.new.1597/coq-8.16.1.tar.gz differ: char 24, line 1 ++++++ coq-refman-8.16.0.tar.xz -> coq-refman-8.16.1.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.16.0.tar.xz /work/SRC/openSUSE:Factory/.coq.new.1597/coq-refman-8.16.1.tar.xz differ: char 27, line 1 ++++++ coq-stdlib-8.16.0.tar.xz -> coq-stdlib-8.16.1.tar.xz ++++++ ++++ 12040 lines of diff (skipped) ++++++ fr.inria.coq.coqide.metainfo.xml ++++++ --- /var/tmp/diff_new_pack.0lx9CL/_old 2022-11-27 12:53:17.499298332 +0100 +++ /var/tmp/diff_new_pack.0lx9CL/_new 2022-11-27 12:53:17.499298332 +0100 @@ -46,6 +46,7 @@ <url type="contribute">https://github.com/coq/coq/blob/master/CONTRIBUTING.md</url> <launchable type="desktop-id">fr.inria.coq.coqide.desktop</launchable> <releases> + <release version="8.16.1" date="2022-11-25"/> <release version="8.16.0" date="2022-09-05"/> <release version="8.15.2" date="2022-05-31"/> <release version="8.15.1" date="2022-03-22"/>
