Julien Puydt pushed to branch upstream at Debian OCaml Maintainers / ssreflect
Commits:
-
a875af1e
by Julien Puydt at 2025-08-24T18:27:40+02:00
-
b107e2e4
by Julien Puydt at 2025-10-14T08:33:34+02:00
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