Julien Puydt pushed to branch upstream at Debian OCaml Maintainers / ssreflect
Commits: c7d3ba49 by Julien Puydt at 2026-07-11T06:36:21+02:00 New upstream version 2.6.0 - - - - - 194 changed files: - .dockerignore - .nix/config.nix - .nix/coq-nix-toolbox.nix - − .nix/coq-overlays/mathcomp-doc/default.nix - − .nix/coq-overlays/mathcomp-single/default.nix - − .nix/coq-overlays/ssprove/default.nix - + .nix/rocq-overlays/mathcomp-doc/default.nix - + .nix/rocq-overlays/mathcomp-single/default.nix - .nix/coq-overlays/mathcomp-warnings/default.nix → .nix/rocq-overlays/mathcomp-warnings/default.nix - CHANGELOG.md - CONTRIBUTING.md - Dockerfile - INSTALL.md - Make - Make.test-suite - Makefile - Makefile.common - − Makefile.coq.local - Makefile.test-suite.coq.local - README.md - _CoqProject - algebra/Make - algebra/Makefile - + algebra/algebra.v - + algebra/algebraic_hierarchy/decfield.v - + algebra/algebraic_hierarchy/divalg.v - algebra/ssralg.v → algebra/algebraic_hierarchy/rings_modules_and_algebras.v - + algebra/algebraic_hierarchy/ssralg.v - algebra/all_algebra.v - algebra/archimedean.v - + algebra/arithmetic_tactic.elpi - + algebra/arithmetic_tactic.v - + algebra/binnums.v - algebra/countalg.v - + algebra/field_tactic.elpi - + algebra/field_tactic.v - algebra/finalg.v - algebra/fraction.v - algebra/intdiv.v - algebra/interval.v - algebra/interval_inference.v - + algebra/lra.v - algebra/matrix.v - algebra/mxalgebra.v - algebra/mxpoly.v - algebra/mxred.v - − algebra/num_theory/orderedzmod.v - algebra/num_theory/numdomain.v → algebra/numeric_hierarchy/numdomain.v - algebra/num_theory/numfield.v → algebra/numeric_hierarchy/numfield.v - + algebra/numeric_hierarchy/orderedzmod.v - algebra/num_theory/ssrnum.v → algebra/numeric_hierarchy/ssrnum.v - algebra/poly.v - algebra/polyXY.v - algebra/polydiv.v - algebra/qpoly.v - algebra/rat.v - + algebra/ring.v - algebra/ring_quotient.v - + algebra/ring_tactic.elpi - + algebra/ring_tactic.v - algebra/sesquilinear.v - algebra/spectral.v - algebra/ssrint.v - + algebra/tensor.v - algebra/vector.v - algebra/zmodp.v - all/Makefile - all/all.v - boot/Make - boot/Makefile - − boot/Makefile.coq.local - boot/all_boot.v - boot/bigop.v - boot/binomial.v - + boot/boot.v - boot/choice.v - boot/div.v - boot/eqtype.v - boot/finfun.v - boot/fingraph.v - boot/finset.v - boot/fintype.v - boot/generic_quotient.v - boot/monoid.v - boot/nmodule.v - boot/path.v - boot/prime.v - boot/seq.v - boot/ssrAC.v - boot/ssrbool.v - boot/ssreflect.v - boot/ssrfun.v - boot/ssrnat.v - boot/tuple.v - coq-mathcomp-character.opam - coq-mathcomp-fingroup.opam - − etc/artwork/coqdoc.css - + etc/artwork/rocqy-mathcomp.png - − etc/buildlibgraph - + etc/rocqnavi_generate-hierarchy-graph.sh - + etc/rocqnavi_index-blacklist - − etc/utils/builddoc_lib.sh - etc/utils/hierarchy.ml - field/Make - field/Makefile - field/algC.v - field/algebraics_fundamentals.v - field/algnum.v - field/all_field.v - field/closed_field.v - field/cyclotomic.v - field/falgebra.v - + field/field.v - field/fieldext.v - field/finfield.v - field/galois.v - field/qfpoly.v - field/separable.v - fingroup/Make → finite_group/Make - character/Makefile → finite_group/Makefile - fingroup/action.v → finite_group/action.v - + finite_group/all_fingroup.v - fingroup/automorphism.v → finite_group/automorphism.v - fingroup/fingroup.v → finite_group/fingroup.v - fingroup/all_fingroup.v → finite_group/finite_group.v - fingroup/gproduct.v → finite_group/gproduct.v - fingroup/morphism.v → finite_group/morphism.v - fingroup/perm.v → finite_group/perm.v - fingroup/presentation.v → finite_group/presentation.v - fingroup/quotient.v → finite_group/quotient.v - character/Make → group_representation/Make - fingroup/Makefile → group_representation/Makefile - + group_representation/all_character.v - character/character.v → group_representation/character.v - character/classfun.v → group_representation/classfun.v - character/all_character.v → group_representation/group_representation.v - character/inertia.v → group_representation/inertia.v - character/integral_char.v → group_representation/integral_char.v - character/mxabelem.v → group_representation/mxabelem.v - character/mxrepresentation.v → group_representation/mxrepresentation.v - character/vcharacter.v → group_representation/vcharacter.v - order/Make - order/Makefile - order/all_order.v - order/order.v - order/preorder.v - rocq-mathcomp-algebra.opam - rocq-mathcomp-boot.opam - rocq-mathcomp-character.opam - rocq-mathcomp-fingroup.opam - + rocq-mathcomp-finite-group.opam - + rocq-mathcomp-group-representation.opam - solvable/Make - solvable/Makefile - solvable/abelian.v - solvable/all_solvable.v - solvable/alt.v - solvable/burnside_app.v - solvable/center.v - solvable/cyclic.v - solvable/extraspecial.v - solvable/extremal.v - solvable/finmodule.v - solvable/frobenius.v - solvable/gfunctor.v - solvable/gseries.v - solvable/hall.v - solvable/jordanholder.v - solvable/maximal.v - solvable/nilpotent.v - solvable/pgroup.v - solvable/primitive_action.v - + solvable/solvable.v - solvable/sylow.v - ssreflect/Make - ssreflect/Makefile - ssreflect/all_ssreflect.v - test_suite/imset2_finset.v - test_suite/imset2_gproduct.v - test_suite/output.v - + test_suite/test_field.v - test_suite/test_guard.v - + test_suite/test_interval_inference.v - + test_suite/test_lra.v - + test_suite/test_micromega.v - test_suite/test_order_conv.v - test_suite/test_rat.v - test_suite/test_regular_conv.v - + test_suite/test_ring.v - + test_suite/test_ring_error.v - + test_suite/test_ring_error.v.out - + test_suite/test_ring_from_sander.v - test_suite/test_ssrAC.v - + test_suite/test_subtype_factories.v The diff was not included because it is too large. View it on GitLab: https://salsa.debian.org/ocaml-team/ssreflect/-/commit/c7d3ba49b3b44a3cb9e4c276dd25f5bbd37898b2 -- View it on GitLab: https://salsa.debian.org/ocaml-team/ssreflect/-/commit/c7d3ba49b3b44a3cb9e4c276dd25f5bbd37898b2 You're receiving this email because of your account on salsa.debian.org. Manage all notifications: https://salsa.debian.org/-/profile/notifications | Help: https://salsa.debian.org/help
