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-03-25 21:54:34 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.1900 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Fri Mar 25 21:54:34 2022 rev:16 rq:964734 version:8.15.1 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2022-01-16 23:19:03.502371383 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.1900/coq.changes 2022-03-25 21:54:38.630276516 +0100 @@ -1,0 +2,12 @@ +Thu Mar 24 22:56:21 UTC 2022 - Aaron Puchert <aaronpuch...@alice-dsl.net> + +- Update to version 8.15.1. + * Fixes an inconsistency when using module subtyping with + inductive types. + * Speeds up CoqIDE on large files. + * Fixes a bug where `coqc -vok` was not creating a .vok file. + * Fixes a regression in `cbn`. + * Improves usability of schemes with `elim foo using scheme with + (P0 := ...)` (the `P0` name was not accessible in 8.15.0). + +------------------------------------------------------------------- Old: ---- coq-8.15.0.tar.gz coq-refman-8.15.0.tar.xz coq-stdlib-8.15.0.tar.xz New: ---- coq-8.15.1.tar.gz coq-refman-8.15.1.tar.xz coq-stdlib-8.15.1.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.V01ev2/_old 2022-03-25 21:54:39.518277362 +0100 +++ /var/tmp/diff_new_pack.V01ev2/_new 2022-03-25 21:54:39.522277366 +0100 @@ -20,7 +20,7 @@ %bcond_without ide Name: coq -Version: 8.15.0 +Version: 8.15.1 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only ++++++ coq-8.15.0.tar.gz -> coq-8.15.1.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/coq-8.15.0.tar.gz /work/SRC/openSUSE:Factory/.coq.new.1900/coq-8.15.1.tar.gz differ: char 28, line 1 ++++++ coq-refman-8.15.0.tar.xz -> coq-refman-8.15.1.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/coq-refman-8.15.0.tar.xz /work/SRC/openSUSE:Factory/.coq.new.1900/coq-refman-8.15.1.tar.xz differ: char 27, line 1 ++++++ coq-stdlib-8.15.0.tar.xz -> coq-stdlib-8.15.1.tar.xz ++++++ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/stdlib/Ltac2.List.html new/stdlib/Ltac2.List.html --- old/stdlib/Ltac2.List.html 2022-01-13 17:57:45.000000000 +0100 +++ new/stdlib/Ltac2.List.html 2022-03-22 18:03:05.000000000 +0100 @@ -536,7 +536,7 @@ <span class="id" title="keyword">let</span> <span class="id" title="var">l</span> := <span class="id" title="var">length</span> <span class="id" title="var">ls</span> <span class="id" title="tactic">in</span><br/> <span class="id" title="var">Control.assert_valid_argument</span> "List.lastn" (<span class="id" title="var">Int.ge</span> <span class="id" title="var">n</span> 0);<br/> <span class="id" title="var">Control.assert_bounds</span> "List.lastn" (<span class="id" title="var">Int.le</span> <span class="id" title="var">n</span> <span class="id" title="var">l</span>);<br/> - <span class="id" title="var">skipn</span> (<span class="id" title="var">Int.sub</span> <span class="id" title="var">l</span> <span class="id" title="var">n</span>).<br/> + <span class="id" title="var">skipn</span> (<span class="id" title="var">Int.sub</span> <span class="id" title="var">l</span> <span class="id" title="var">n</span>) <span class="id" title="var">ls</span>.<br/> <br/> <span class="id" title="keyword">Ltac</span>2 <span class="id" title="keyword">rec</span> <span class="id" title="var">nodup</span> (<span class="id" title="var">eqb</span> : '<span class="id" title="var">a</span> -> '<span class="id" title="var">a</span> -> <span class="id" title="var">bool</span>) (<span class="id" title="var">ls</span> : '<span class="id" title="var">a</span> <span class="id" title="var">list</span>) :=<br/>
