Julien Puydt pushed to branch upstream at Debian OCaml Maintainers / ssreflect
Commits: a875af1e by Julien Puydt at 2025-08-24T18:27:40+02:00 New upstream version 2.4.0 - - - - - b107e2e4 by Julien Puydt at 2025-10-14T08:33:34+02:00 New upstream version 2.5.0 - - - - - 224 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 - 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: https://salsa.debian.org/ocaml-team/ssreflect/-/compare/545ac756611ba317587dd2969178d93d7ff89949...b107e2e480d05f7ab868c8d3bf09c422ebda8636 -- View it on GitLab: https://salsa.debian.org/ocaml-team/ssreflect/-/compare/545ac756611ba317587dd2969178d93d7ff89949...b107e2e480d05f7ab868c8d3bf09c422ebda8636 You're receiving this email because of your account on salsa.debian.org.
