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-09-21 12:03:33 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/coq (Old) and /work/SRC/openSUSE:Factory/.coq.new.383539 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "coq" Mon Sep 21 12:03:33 2026 rev:34 rq:1379139 version:9.3.0 Changes: -------- --- /work/SRC/openSUSE:Factory/coq/coq.changes 2026-08-04 21:38:36.040941437 +0200 +++ /work/SRC/openSUSE:Factory/.coq.new.383539/coq.changes 2026-09-21 12:03:59.220171431 +0200 @@ -1,0 +2,31 @@ +Sat Sep 19 21:08:33 UTC 2026 - Aaron Puchert <[email protected]> + +- Update to version 9.3.0. + * Require dune version 3.21.0 to support the rocq.theory stanza. + * New notion of Rocq package and installation layout supported by + a new command-line option -package DEP that automatically adds + the correct -Q options for DEP and its transitive dependencies. + For backwards compatibility, the old installation scheme + targeting the coq/user-contrib directory is kept (see also Rocq + makefile documentation for --rocq-package). + * New syntactic sugar {| t with n := v |} to provide default + values for omitted fields in a record value. + * New OCaml-inspired @@ and |> notations in Ltac2. + * New syntactic sugar for match with one interesting case. For + example `if g is c then t else e` stands for `match g with c => + t | _ => e end`. + * New syntactic sugars `& T` for anonymous binders `(_ : T)` and + `of T & ... & T` for anonymous binders in constructors, + enabling Variant `t := C1 of a & b & c | C2 x y of P x & Q y`. + * SSReflect rewrite tactic renamed into `rw`, the old name is + still available via `Import ssreflect`. + * New `AllocLimit` and `alloc_limit` to enforce allocation limits + during execution. + * Extend generation of eliminators to handle nesting with + Primitive Arrays. + * New Alectryon Markdown backend for `rocq doc`. + * Fixed confusion between section variables and goal hypotheses + with the same name, which made clearing section variables very + buggy. + +------------------------------------------------------------------- Old: ---- rocq-9.2.0.tar.gz rocq-corelib-doc-9.2.0.tar.xz rocq-refman-9.2.0.tar.xz New: ---- rocq-9.3.0.tar.gz rocq-corelib-doc-9.3.0.tar.xz rocq-refman-9.3.0.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ coq.spec ++++++ --- /var/tmp/diff_new_pack.VIymLn/_old 2026-09-21 12:04:37.236759645 +0200 +++ /var/tmp/diff_new_pack.VIymLn/_new 2026-09-21 12:04:37.238759719 +0200 @@ -28,7 +28,7 @@ %endif Name: coq -Version: 9.2.0 +Version: 9.3.0 Release: 0 Summary: Proof Assistant based on the Calculus of Inductive Constructions License: LGPL-2.1-only @@ -46,7 +46,7 @@ BuildRequires: make >= 3.81 BuildRequires: ocaml >= 4.09.0 BuildRequires: ocaml-camlp5-devel >= 5.08 -BuildRequires: ocaml-dune >= 3.8.3 +BuildRequires: ocaml-dune >= 3.21.0 BuildRequires: ocaml-rpm-macros BuildRequires: ocamlfind(findlib) BuildRequires: ocamlfind(zarith) ++++++ rocq-9.2.0.tar.gz -> rocq-9.3.0.tar.gz ++++++ /work/SRC/openSUSE:Factory/coq/rocq-9.2.0.tar.gz /work/SRC/openSUSE:Factory/.coq.new.383539/rocq-9.3.0.tar.gz differ: char 13, line 1 ++++++ rocq-corelib-doc-9.2.0.tar.xz -> rocq-corelib-doc-9.3.0.tar.xz ++++++ ++++ 45558 lines of diff (skipped) ++++++ rocq-refman-9.2.0.tar.xz -> rocq-refman-9.3.0.tar.xz ++++++ /work/SRC/openSUSE:Factory/coq/rocq-refman-9.2.0.tar.xz /work/SRC/openSUSE:Factory/.coq.new.383539/rocq-refman-9.3.0.tar.xz differ: char 15, line 1
