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-09-09 18:28:00 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.2083 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Fri Sep 9 18:28:00 2022 rev:18 rq:1002206 version:8.16.0 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2022-06-02 21:54:28.988389493 +0200 +++ /work/SRC/openSUSE:Factory/.coq.new.2083/coq.changes 2022-09-09 18:29:30.801265719 +0200 @@ -1,0 +2,27 @@ +Thu Sep 8 21:11:24 UTC 2022 - Aaron Puchert <[email protected]> + +- Update to version 8.16.0. + * The guard checker (see `Guarded`) now ensures strong + normalization under any reduction strategy. + * Irrelevant terms (in the `SProp` sort) are now squashed to a + dummy value during conversion, fixing a subject reduction + issue and making proof conversion faster. + * Introduction of reversible coercions, which allow coercions + relying on meta-level resolution such as type-classes or + canonical structures. Also allow coercions that do not fullfill + the uniform inheritance condition. + * Generalized rewriting support for rewriting with `Type`-valued + relations and in `Type` contexts, using the + `Classes.CMorphisms` library. + * Added the boolean equality scheme command for decidable + inductive types. + * Added a `Print Notation` command. + * Incompatibilities in name generation for Program obligations, + `eauto` treatment of tactic failure levels, use of `ident` in + notations, parsing of module expressions. + * Standard library reorganization and deprecations. + * Improve the treatment of standard library numbers by + `Extraction`. +- Coq requires ocamlfind at runtime now. + +------------------------------------------------------------------- Old: ---- coq-8.15.2.tar.gz coq-refman-8.15.2.tar.xz coq-stdlib-8.15.2.tar.xz New: ---- coq-8.16.0.tar.gz coq-refman-8.16.0.tar.xz coq-stdlib-8.16.0.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.D30Mzy/_old 2022-09-09 18:29:31.397267288 +0200 +++ /var/tmp/diff_new_pack.D30Mzy/_new 2022-09-09 18:29:31.401267298 +0200 @@ -20,7 +20,7 @@ %bcond_without ide Name: coq -Version: 8.15.2 +Version: 8.16.0 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only @@ -35,7 +35,7 @@ Source100: %{name}-rpmlintrc BuildRequires: desktop-file-utils BuildRequires: make >= 3.81 -BuildRequires: ocaml >= 4.05.0 +BuildRequires: ocaml >= 4.09.0 BuildRequires: ocaml-camlp5-devel >= 5.08 BuildRequires: ocaml-dune >= 2.5.1 BuildRequires: ocamlfind(findlib) @@ -44,6 +44,7 @@ BuildRequires: update-desktop-files BuildRequires: ocamlfind(lablgtk3-sourceview3) %endif +Requires: ocamlfind %description Proof assistant which allows to handle calculus assertions, check mechanically @@ -65,8 +66,7 @@ Summary: Development files for coq Group: Development/Libraries/Other Requires: %{name} = %{version} -Requires: ocaml >= 4.05.0 -Requires: ocamlfind(findlib) +Requires: ocaml >= 4.09.0 %description devel This package contains development files for Coq. ++++++ coq-8.15.2.tar.gz -> coq-8.16.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.15.2.tar.gz /work/SRC/openSUSE:Factory/.coq.new.2083/coq-8.16.0.tar.gz differ: char 27, line 1 ++++++ coq-refman-8.15.2.tar.xz -> coq-refman-8.16.0.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.15.2.tar.xz /work/SRC/openSUSE:Factory/.coq.new.2083/coq-refman-8.16.0.tar.xz differ: char 26, line 1 ++++++ coq-stdlib-8.15.2.tar.xz -> coq-stdlib-8.16.0.tar.xz ++++++ ++++ 162410 lines of diff (skipped) ++++++ fr.inria.coq.coqide.metainfo.xml ++++++ --- /var/tmp/diff_new_pack.D30Mzy/_old 2022-09-09 18:29:32.997271499 +0200 +++ /var/tmp/diff_new_pack.D30Mzy/_new 2022-09-09 18:29:33.001271509 +0200 @@ -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.0" date="2022-09-05"/> <release version="8.15.2" date="2022-05-31"/> <release version="8.15.1" date="2022-03-22"/> </releases>
