[Git][ocaml-team/ssreflect][master] 10 commits: New upstream version 2.4.0

["Julien Puydt (@jpuydt)" <gitlab@salsa.debian.org>]

Title: GitLab

Julien Puydt pushed to branch master at Debian OCaml Maintainers / ssreflect

Commits:

• a875af1e
  by Julien Puydt at 2025-08-24T18:27:40+02:00

  New upstream version 2.4.0

• b49b9b1e
  by Julien Puydt at 2025-08-26T21:01:49+02:00

  New upstream version 2.4.0

• 2ee8e22b
  by Julien Puydt at 2025-08-26T22:17:55+02:00

  Package new upstream 2.4.0
  

• 4e875d86
  by Julien Puydt at 2025-08-26T22:17:55+02:00

  Bump standards-version to 4.7.2
  

• e13a7646
  by Julien Puydt at 2025-08-29T08:06:41+02:00

  Fix documentation building
  

• b107e2e4
  by Julien Puydt at 2025-10-14T08:33:34+02:00

  New upstream version 2.5.0

• fa9ff59f
  by Julien Puydt at 2025-10-14T08:33:38+02:00

  Update upstream source from tag 'upstream/2.5.0'
  
  Update to upstream version '2.5.0'
  with Debian dir b19ad9e9a57d7ec02f0618a545674dd9d1959367

• 40df56f0
  by Julien Puydt at 2025-10-14T14:09:22+02:00

  Package new upstream 2.5.0
  

• d2edc642
  by Julien Puydt at 2025-10-29T10:27:08+01:00

  Drop useless dbgsym packages
  

• a7861de5
  by Julien Puydt at 2025-10-29T10:27:27+01:00

  Prepare for upload to experimental
  

235 changed files:

• .dockerignore
• .nix/config.nix
• .nix/coq-nix-toolbox.nix
• − .nix/coq-overlays/extructures/default.nix
• .nix/coq-overlays/mathcomp-warnings/default.nix
• + .nix/coq-overlays/ssprove/default.nix
• .vscode/settings.json
• CHANGELOG.md
• − CHANGELOG_UNRELEASED.md
• CONTRIBUTING.md
• Dockerfile
• Dockerfile.make
• INSTALL.md
• CeCILL-B → LICENCE
• mathcomp/Make → Make
• mathcomp/Make.test-suite → Make.test-suite
• mathcomp/Makefile → Makefile
• mathcomp/Makefile.common → Makefile.common
• + Makefile.coq.local
• mathcomp/Makefile.test-suite.coq.local → Makefile.test-suite.coq.local
• README.md
• _CoqProject
• mathcomp/algebra/Make → algebra/Make
• mathcomp/algebra/Makefile → algebra/Makefile
• + algebra/all_algebra.v
• mathcomp/algebra/archimedean.v → algebra/archimedean.v
• mathcomp/algebra/countalg.v → algebra/countalg.v
• mathcomp/algebra/finalg.v → algebra/finalg.v
• mathcomp/algebra/fraction.v → algebra/fraction.v
• mathcomp/algebra/intdiv.v → algebra/intdiv.v
• mathcomp/algebra/interval.v → algebra/interval.v
• + algebra/interval_inference.v
• mathcomp/algebra/matrix.v → algebra/matrix.v
• mathcomp/algebra/mxalgebra.v → algebra/mxalgebra.v
• mathcomp/algebra/mxpoly.v → algebra/mxpoly.v
• mathcomp/algebra/mxred.v → algebra/mxred.v
• mathcomp/algebra/ssrnum.v → algebra/num_theory/numdomain.v
• + algebra/num_theory/numfield.v
• + algebra/num_theory/orderedzmod.v
• + algebra/num_theory/ssrnum.v
• mathcomp/algebra/poly.v → algebra/poly.v
• mathcomp/algebra/polyXY.v → algebra/polyXY.v
• mathcomp/algebra/polydiv.v → algebra/polydiv.v
• mathcomp/algebra/qpoly.v → algebra/qpoly.v
• mathcomp/algebra/rat.v → algebra/rat.v
• mathcomp/algebra/ring_quotient.v → algebra/ring_quotient.v
• mathcomp/algebra/sesquilinear.v → algebra/sesquilinear.v
• mathcomp/algebra/spectral.v → algebra/spectral.v
• mathcomp/algebra/ssralg.v → algebra/ssralg.v
• mathcomp/algebra/ssrint.v → algebra/ssrint.v
• mathcomp/algebra/vector.v → algebra/vector.v
• mathcomp/algebra/zmodp.v → algebra/zmodp.v
• mathcomp/all/Makefile → all/Makefile
• + all/all.v
• mathcomp/ssreflect/Make → boot/Make
• mathcomp/ssreflect/Makefile → boot/Makefile
• + boot/Makefile.coq.local
• mathcomp/ssreflect/all_ssreflect.v → boot/all_boot.v
• mathcomp/ssreflect/bigop.v → boot/bigop.v
• mathcomp/ssreflect/binomial.v → boot/binomial.v
• mathcomp/ssreflect/choice.v → boot/choice.v
• mathcomp/ssreflect/div.v → boot/div.v
• mathcomp/ssreflect/eqtype.v → boot/eqtype.v
• mathcomp/ssreflect/finfun.v → boot/finfun.v
• mathcomp/ssreflect/fingraph.v → boot/fingraph.v
• mathcomp/ssreflect/finset.v → boot/finset.v
• mathcomp/ssreflect/fintype.v → boot/fintype.v
• mathcomp/ssreflect/generic_quotient.v → boot/generic_quotient.v
• + boot/monoid.v
• + boot/nmodule.v
• mathcomp/ssreflect/path.v → boot/path.v
• mathcomp/ssreflect/prime.v → boot/prime.v
• mathcomp/ssreflect/seq.v → boot/seq.v
• mathcomp/ssreflect/ssrAC.v → boot/ssrAC.v
• mathcomp/ssreflect/ssrbool.v → boot/ssrbool.v
• + boot/ssreflect.v
• mathcomp/ssreflect/ssrfun.v → boot/ssrfun.v
• + boot/ssrmatching.v
• mathcomp/ssreflect/ssrnat.v → boot/ssrnat.v
• mathcomp/ssreflect/ssrnotations.v → boot/ssrnotations.v
• mathcomp/ssreflect/tuple.v → boot/tuple.v
• mathcomp/character/Make → character/Make
• mathcomp/character/Makefile → character/Makefile
• mathcomp/character/all_character.v → character/all_character.v
• mathcomp/character/character.v → character/character.v
• mathcomp/character/classfun.v → character/classfun.v
• mathcomp/character/inertia.v → character/inertia.v
• mathcomp/character/integral_char.v → character/integral_char.v
• mathcomp/character/mxabelem.v → character/mxabelem.v
• mathcomp/character/mxrepresentation.v → character/mxrepresentation.v
• mathcomp/character/vcharacter.v → character/vcharacter.v
• coq-mathcomp-algebra.opam
• + coq-mathcomp-boot.opam
• coq-mathcomp-character.opam
• coq-mathcomp-field.opam
• coq-mathcomp-fingroup.opam
• + coq-mathcomp-order.opam
• coq-mathcomp-solvable.opam
• coq-mathcomp-ssreflect.opam
• debian/changelog
• debian/control
• + debian/libcoq-mathcomp-boot.install.in
• + debian/libcoq-mathcomp-order.install.in
• debian/libcoq-mathcomp.docs
• − debian/libcoq-mathcomp.examples
• − debian/libcoq-mathcomp.lintian-overrides
• debian/libcoq-mathcomp.doc-base → debian/mathcomp-doc.doc-base
• + debian/mathcomp-doc.docs
• + debian/mathcomp-doc.lintian-overrides
• debian/rules
• default.nix
• + doc/changelog/01-added/00000-title.md
• + doc/changelog/02-changed/00000-title.md
• + doc/changelog/03-renamed/00000-title.md
• + doc/changelog/04-removed/00000-title.md
• + doc/changelog/05-deprecated/00000-title.md
• + doc/changelog/README.md
• + doc/changelog/generate-release-changelog.sh
• + doc/changelog/make-entry.sh
• etc/utils/builddoc_lib.sh
• etc/utils/packager
• + etc/utils/perf.sh
• mathcomp/field/Make → field/Make
• mathcomp/field/Makefile → field/Makefile
• mathcomp/field/algC.v → field/algC.v
• mathcomp/field/algebraics_fundamentals.v → field/algebraics_fundamentals.v
• mathcomp/field/algnum.v → field/algnum.v
• + field/all_field.v
• mathcomp/field/closed_field.v → field/closed_field.v
• mathcomp/field/cyclotomic.v → field/cyclotomic.v
• mathcomp/field/falgebra.v → field/falgebra.v
• mathcomp/field/fieldext.v → field/fieldext.v
• mathcomp/field/finfield.v → field/finfield.v
• mathcomp/field/galois.v → field/galois.v
• mathcomp/field/qfpoly.v → field/qfpoly.v
• mathcomp/field/separable.v → field/separable.v
• mathcomp/fingroup/Make → fingroup/Make
• mathcomp/fingroup/Makefile → fingroup/Makefile
• mathcomp/fingroup/action.v → fingroup/action.v
• + fingroup/all_fingroup.v
• mathcomp/fingroup/automorphism.v → fingroup/automorphism.v
• mathcomp/fingroup/fingroup.v → fingroup/fingroup.v
• mathcomp/fingroup/gproduct.v → fingroup/gproduct.v
• mathcomp/fingroup/morphism.v → fingroup/morphism.v
• mathcomp/fingroup/perm.v → fingroup/perm.v
• mathcomp/fingroup/presentation.v → fingroup/presentation.v
• mathcomp/fingroup/quotient.v → fingroup/quotient.v
• − mathcomp/_CoqProject
• − mathcomp/algebra/AUTHORS
• − mathcomp/algebra/CeCILL-B
• − mathcomp/algebra/INSTALL.md
• − mathcomp/algebra/README.md
• − mathcomp/algebra/all_algebra.v
• − mathcomp/all/all.v
• − mathcomp/character/AUTHORS
• − mathcomp/character/CeCILL-B
• − mathcomp/character/INSTALL.md
• − mathcomp/character/README.md
• − mathcomp/field/AUTHORS
• − mathcomp/field/CeCILL-B
• − mathcomp/field/INSTALL.md
• − mathcomp/field/README.md
• − mathcomp/field/all_field.v
• − mathcomp/fingroup/AUTHORS
• − mathcomp/fingroup/CeCILL-B
• − mathcomp/fingroup/INSTALL.md
• − mathcomp/fingroup/README.md
• − mathcomp/fingroup/all_fingroup.v
• − mathcomp/solvable/AUTHORS
• − mathcomp/solvable/CeCILL-B
• − mathcomp/solvable/INSTALL.md
• − mathcomp/solvable/README.md
• − mathcomp/solvable/all_solvable.v
• − mathcomp/ssreflect/AUTHORS
• − mathcomp/ssreflect/CeCILL-B
• − mathcomp/ssreflect/INSTALL.md
• − mathcomp/ssreflect/INSTALL.pg
• − mathcomp/ssreflect/README.md
• − mathcomp/ssreflect/pg-ssr.el
• − mathcomp/ssreflect/ssreflect.v
• − mathcomp/ssreflect/ssrmatching.v
• − mathcomp/test_suite/output.v.out.8.7
• − mathcomp/test_suite/output.v.out.8.8
• − mathcomp/test_suite/output.v.out.8.9
• + order/Make
• + order/Makefile
• + order/all_order.v
• mathcomp/ssreflect/order.v → order/order.v
• + order/preorder.v
• + rocq-mathcomp-algebra.opam
• + rocq-mathcomp-boot.opam
• + rocq-mathcomp-character.opam
• + rocq-mathcomp-field.opam
• + rocq-mathcomp-fingroup.opam
• + rocq-mathcomp-order.opam
• + rocq-mathcomp-solvable.opam
• + rocq-mathcomp-ssreflect.opam
• mathcomp/solvable/Make → solvable/Make
• mathcomp/solvable/Makefile → solvable/Makefile
• mathcomp/solvable/abelian.v → solvable/abelian.v
• + solvable/all_solvable.v
• mathcomp/solvable/alt.v → solvable/alt.v
• mathcomp/solvable/burnside_app.v → solvable/burnside_app.v
• mathcomp/solvable/center.v → solvable/center.v
• mathcomp/solvable/commutator.v → solvable/commutator.v
• mathcomp/solvable/cyclic.v → solvable/cyclic.v
• mathcomp/solvable/extraspecial.v → solvable/extraspecial.v
• mathcomp/solvable/extremal.v → solvable/extremal.v
• mathcomp/solvable/finmodule.v → solvable/finmodule.v
• mathcomp/solvable/frobenius.v → solvable/frobenius.v
• mathcomp/solvable/gfunctor.v → solvable/gfunctor.v
• mathcomp/solvable/gseries.v → solvable/gseries.v
• mathcomp/solvable/hall.v → solvable/hall.v
• mathcomp/solvable/jordanholder.v → solvable/jordanholder.v
• mathcomp/solvable/maximal.v → solvable/maximal.v
• mathcomp/solvable/nilpotent.v → solvable/nilpotent.v
• mathcomp/solvable/pgroup.v → solvable/pgroup.v
• mathcomp/solvable/primitive_action.v → solvable/primitive_action.v
• mathcomp/solvable/sylow.v → solvable/sylow.v
• + ssreflect/Make
• + ssreflect/Makefile
• + ssreflect/all_ssreflect.v
• mathcomp/test_suite/imset2_finset.v → test_suite/imset2_finset.v
• mathcomp/test_suite/imset2_finset.v.out → test_suite/imset2_finset.v.out
• mathcomp/test_suite/imset2_gproduct.v → test_suite/imset2_gproduct.v
• mathcomp/test_suite/imset2_gproduct.v.out → test_suite/imset2_gproduct.v.out
• mathcomp/test_suite/output.v → test_suite/output.v
• mathcomp/test_suite/output.v.out → test_suite/output.v.out
• mathcomp/test_suite/test_guard.v → test_suite/test_guard.v
• mathcomp/test_suite/test_intro_rw.v → test_suite/test_intro_rw.v
• mathcomp/test_suite/test_order_conv.v → test_suite/test_order_conv.v
• mathcomp/test_suite/test_rat.v → test_suite/test_rat.v
• mathcomp/test_suite/test_rat.v.out → test_suite/test_rat.v.out
• mathcomp/test_suite/test_regular_conv.v → test_suite/test_regular_conv.v
• mathcomp/test_suite/test_ssrAC.v → test_suite/test_ssrAC.v

The diff was not included because it is too large.

—
View it on GitLab.
You're receiving this email because of your account on salsa.debian.org. Manage all notifications · Help Notification message regarding https://salsa.debian.org/ocaml-team/ssreflect/-/compare/f98982514cb1360225753067a9eff1e237142e84...a7861de52e00df20a96249be90cf3353a3f6c153 at 1761730078