Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package coq for openSUSE:Factory checked in at 2026-04-01 19:51:55 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.21863 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Wed Apr 1 19:51:55 2026 rev:32 rq:1343994 version:9.2.0 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2026-03-23 17:14:16.559939785 +0100 +++ /work/SRC/openSUSE:Factory/.coq.new.21863/coq.changes 2026-04-01 19:53:18.763819881 +0200 @@ -1,0 +2,38 @@ +Tue Mar 31 21:41:58 UTC 2026 - Aaron Puchert <[email protected]> + +- Update to version 9.2.0. + * Reenable support for `native_compute` when compiled with + OCaml 5. As it relies on some architecture-specific code, only + some x86 setups are supported for now. + * Records in `Type` and `Prop`, with only fields in `SProp`, can + now have primitive projections but without eta conversion. + * Implicit elaboration of elimination constraints. + * Parsing of elimination constraints in prenex polymorphic + definitions as well as in constraints declaration + `Constraint s1 -> s2`. + * Induction hypotheses are now generated for nested arguments + provided an `All` predicate, and a theorem to prove it, have + been registered with the keys `All` and `AllForall`. + * Add a `Scheme All` command to generate the All predicate and + its theorem for inductive types used for the eliminators of + nested inductive types. + * Tactics such as `induction` find eliminators (like `nat_rect`) + through the `Register Scheme` table (which is automatically + populated by `Scheme` and automatic scheme declarations) + instead of by name (the lookup by name remains for now for + backward compatibility). + * Attribute `schemes` to control automatic scheme declaration. + * Goal names can be automatically generated for `induction`, + `destruct` and `eapply` by using the `Generate Goal Names` flag. + * Congruence tactics now handle primitive ints, floats and + strings. + * `Ltac2 Custom Entry` making it possible to define more complex + `Ltac2 Notation`s and many other additions to `Ltac2` (see + documentation for details). + * `Printing Fully Qualified` to print all names (global + references, modules, module types, universes, etc) using fully + qualified paths. + * Generalized universe polymorphism flag structure (ML API + change). + +------------------------------------------------------------------- Old: ---- rocq-9.1.1.tar.gz rocq-corelib-doc-9.1.1.tar.xz rocq-refman-9.1.1.tar.xz New: ---- rocq-9.2.0.tar.gz rocq-corelib-doc-9.2.0.tar.xz rocq-refman-9.2.0.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.WiAfw2/_old 2026-04-01 19:53:21.439931036 +0200 +++ /var/tmp/diff_new_pack.WiAfw2/_new 2026-04-01 19:53:21.439931036 +0200 @@ -28,7 +28,7 @@ %endif Name: coq -Version: 9.1.1 +Version: 9.2.0 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only @@ -126,7 +126,6 @@ ./configure \ -prefix %{_prefix} \ -libdir %{_libdir}/coq \ - -mandir %{_mandir} \ -datadir %{_datadir}/%{_name} \ -docdir %{_docdir}/%{_name} \ -configdir %{_sysconfdir}/xdg/%{_name} \ @@ -191,10 +190,10 @@ # cd V%{version} # tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \ # --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \ -# -cJf ../../coq-refman-%{version}.tar.xz refman +# -cJf ../../rocq-refman-%{version}.tar.xz refman # tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \ # --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \ -# -cJf ../../coq-corelib-doc-%{version}.tar.xz corelib +# -cJf ../../rocq-corelib-doc-%{version}.tar.xz corelib # popd # Slim down documentation pages, add some margin directly. ++++++ rocq-9.1.1.tar.gz -> rocq-9.2.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/rocq-9.1.1.tar.gz /work/SRC/openSUSE:Factory/.coq.new.21863/rocq-9.2.0.tar.gz differ: char 12, line 1 ++++++ rocq-corelib-doc-9.1.1.tar.xz -> rocq-corelib-doc-9.2.0.tar.xz ++++++ ++++ 94613 lines of diff (skipped) ++++++ rocq-refman-9.1.1.tar.xz -> rocq-refman-9.2.0.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/rocq-refman-9.1.1.tar.xz /work/SRC/openSUSE:Factory/.coq.new.21863/rocq-refman-9.2.0.tar.xz differ: char 15, line 1
