Stéphane Glondu pushed to branch upstream at Debian OCaml Maintainers / hol-light
Commits: 7da7ef10 by Stephane Glondu at 2026-07-02T15:39:12+02:00 New upstream snapshot 3.1.0+git20260609 - - - - - 124 changed files: - + .github/dependabot.yml - .github/workflows/main.yml - + .github/workflows/mcp.yml - .gitignore - + 100/buffon.ml - + 100/cubedissection.ml - + 100/green.ml - 100/isoperimetric.ml - 100/transcendence.ml - CHANGES - + Examples/doomsday.ml - Help/UNIFY_ACCEPT_TAC.hlp - + Help/UNIFY_REFL_TAC.hlp - Help/list_mk_exists.hlp - + Help/mapi.hlp - Help/new_basic_type_definition.hlp - Help/new_type_definition.hlp - Jordan/jordan_curve_theorem.ml - Jordan/metric_spaces.ml - Jordan/misc_defs_and_lemmas.ml - Jordan/tactics_ext2.ml - Library/bitmatch.ml - Library/calc_real.ml - + Library/components.ml - Library/fieldtheory.ml - Library/grouptheory.ml - Library/isum.ml - Library/permutations.ml - + Library/rabin_test.ml - + Library/records.ml - Library/ringtheory.ml - + Library/symmetric_group.ml - + Library/tactician_light.ml - Library/words.ml - META - Makefile - Multivariate/cauchy.ml - Multivariate/complex_database.ml - Multivariate/lpspaces.ml - Multivariate/measure.ml - Multivariate/metric.ml - Multivariate/multivariate_database.ml - + Multivariate/paracompact.ml - Multivariate/paths.ml - Multivariate/realanalysis.ml - Multivariate/topology.ml - Multivariate/transcendentals.ml - Multivariate/vectors.ml - + Probability/characteristic_functions.ml - + Probability/clt.ml - + Probability/distributions.ml - + Probability/ergodic.ml - + Probability/expectation.ml - + Probability/independence.ml - + Probability/make.ml - + Probability/martingale_convergence.ml - + Probability/martingales.ml - + Probability/measure.ml - + Probability/random_variables.ml - README - + TacticTrace/.gitignore - + TacticTrace/Makefile - + TacticTrace/README.md - + TacticTrace/build-hol-kernel.sh - + TacticTrace/examples/conv.answer/ACCEPT_TAC.json - + TacticTrace/examples/conv.answer/CONV_TAC.json - + TacticTrace/examples/conv.answer/NUM_REDUCE_CONV.json - + TacticTrace/examples/conv.answer/simple_conv.json - + TacticTrace/examples/conv.answer/simple_conv3.json - + TacticTrace/examples/conv.answer/simple_conv4.json - + TacticTrace/examples/conv.ml - + TacticTrace/examples/tactic.answer/ALL_TAC.json - + TacticTrace/examples/tactic.answer/REFL_TAC.json - + TacticTrace/examples/tactic.answer/repeat_tac.json - + TacticTrace/examples/tactic.answer/simple_tac.json - + TacticTrace/examples/tactic.answer/tac1.json - + TacticTrace/examples/tactic.answer/tac2.json - + TacticTrace/examples/tactic.answer/tac_arg.json - + TacticTrace/examples/tactic.answer/tac_in_let.json - + TacticTrace/examples/tactic.ml - + TacticTrace/exportTrace.ml - + TacticTrace/get-ast.sh - + TacticTrace/modify-proof.sh - + TacticTrace/ocamlTypes.ml - + TacticTrace/remove-linenum-dirs.py - + TacticTrace/tracer.ml - + TacticTrace/types_lexer.mll - + TacticTrace/types_parser.mly - + TacticTrace/types_test.ml - unit_tests.ml → UnitTests/basic_tests.ml - + UnitTests/printer_tests.ml - calc_int.ml - calc_num.ml - calc_rat.ml - hol_4.14.sh - − holtest - holtest.mk - holtest_parallel - inline_load.ml - int.ml - itab.ml - iterate.ml - lib.ml - + mcp/.python-version - + mcp/README.md - + mcp/SKILL.md - + mcp/TUTORIAL.md - + mcp/hol-mcp.toml - + mcp/make_checkpoint.py - + mcp/mcp_helpers.ml - + mcp/pyproject.toml - + mcp/server.py - + mcp/smoke_test.py - + mcp/test_server.py - + mcp/uv.lock - metis.ml - opam - + pa_j/chooser.sh - + pa_j/pa_j_4.xx_8.03.06.ml - + pa_j/pa_j_5.4_8.04.00.ml - printer.ml - sets.ml - + update_database/chooser.sh - + update_database/update_database_5.4.ml The diff was not included because it is too large. View it on GitLab: https://salsa.debian.org/ocaml-team/hol-light/-/commit/7da7ef104f69b7f677aada1228b9484769f2f052 -- View it on GitLab: https://salsa.debian.org/ocaml-team/hol-light/-/commit/7da7ef104f69b7f677aada1228b9484769f2f052 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
