Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2023-09-20 13:25:12 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.16627 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Wed Sep 20 13:25:12 2023 rev:23 rq:1111685 version:8.18.0 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2023-06-29 17:29:14.618581017 +0200 +++ /work/SRC/openSUSE:Factory/.coq.new.16627/coq.changes 2023-09-20 13:26:44.797394139 +0200 @@ -1,0 +2,19 @@ +Sat Sep 16 20:35:51 UTC 2023 - Aaron Puchert <[email protected]> + +- Update to version 8.18.0. + * The default locality of `Hint` and `Instance` commands was + switched to `export`. + * The universe unification algorithm can now delay the commitment + to a sort (the algorithm used to pick `Type`). Thanks to this + feature many `Prop` and `SProp` annotations can be now omitted. + * Ltac2 supports array literals, maps and sets of primitive + datatypes such as names (of constants, inductive types, etc) + and fine-grained control over profiling. + * The warning system offers new categories, enabling finer + (de)activation of specific warnings. This should be + particularly useful to handle deprecations. + * Many new lemmas useful for teaching analysis with Coq are now + part of the standard library about real numbers. + * The `#[deprecated]` attribute can now be applied to definitions. + +------------------------------------------------------------------- Old: ---- coq-8.17.1.tar.gz coq-refman-8.17.1.tar.xz coq-stdlib-8.17.1.tar.xz New: ---- coq-8.18.0.tar.gz coq-refman-8.18.0.tar.xz coq-stdlib-8.18.0.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.KovE7I/_old 2023-09-20 13:26:46.365450316 +0200 +++ /var/tmp/diff_new_pack.KovE7I/_new 2023-09-20 13:26:46.365450316 +0200 @@ -26,7 +26,7 @@ %endif Name: coq -Version: 8.17.1 +Version: 8.18.0 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only @@ -201,6 +201,7 @@ %{_bindir}/coqdoc %{_bindir}/coqnative %{_bindir}/coqpp +%{_bindir}/coqtimelog2html %{_bindir}/coqtop %{_bindir}/coqtop.byte %{_bindir}/coqtop.opt ++++++ coq-8.17.1.tar.gz -> coq-8.18.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.17.1.tar.gz /work/SRC/openSUSE:Factory/.coq.new.16627/coq-8.18.0.tar.gz differ: char 28, line 1 ++++++ coq-refman-8.17.1.tar.xz -> coq-refman-8.18.0.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.17.1.tar.xz /work/SRC/openSUSE:Factory/.coq.new.16627/coq-refman-8.18.0.tar.xz differ: char 26, line 1 ++++++ coq-stdlib-8.17.1.tar.xz -> coq-stdlib-8.18.0.tar.xz ++++++ ++++ 234705 lines of diff (skipped)
