Release 2026.06

What's Changed

• Added exact lemma for parameteriezed global hybrids. by @alleystoughton in #992
• ci: enforce single-commit PRs by @strub in #1003
• subtype: generalize over section-declared free types at section close by @strub in #1002
• Check that Distr is in scope when tagging distributions, fixing #211 by @oskgo in #988
• Refactor CI to run in fresh build box by @fdupress in #1000
• [provers] update all CVC5 versions by @fdupress in #1004
• [docker] use binary alt-ergo builds by @fdupress in #1010
• Emit proper error message when typing ={pvar} in a single sided context by @oskgo in #1013
• Prevent type parameters in subtypes by @oskgo in #1012
• [docker] consolidate dockerfiles by @fdupress in #1007
• split: add split * and split + to iterate over top-level conjunctions by @strub in #1015
• Cloning: support inlining a type via clone-inline (clinline) by @strub in #1021
• PHL: make eqobs-in programmatically reusable (split parse/tactic) by @strub in #1023
• congr: add congr pat and congr * variants by @strub in #1016
• bullets: focusing operators behind +strict_bullets pragma by @strub in #1017
• [runtest] list failing files by @fdupress in #1032
• Switch axiom replay to use exact rather than a custom apply variant by @oskgo in #1029
• Check equality of expressions up to convertibility by @oskgo in #996
• Bugfix: form_read track Fglob like Fpvar by @Gustavo2622 in #987
• [ci] do not rebuild base or base-build in PR runs by @fdupress in #1008
• Simplify some smt calls by @oskgo in #1025
• [ci] hotfix for the one untested path in docker PR by @fdupress in #1035
• ecall: avoid internal name collision in abstract_pvs by @strub in #1038
• proc change: well-formed goals when introducing fresh locals by @strub in #1040
• feat(phl): support backward ecall on bdHoare/phoare goals by @mbbarbosa in #1031
• Warn on useless unfolds by default by @oskgo in #1034
• smt: add [smt_inline] operator tag to δ/β-reduce at use sites by @strub in #1039
• typing: resolve record projections from the record type by @strub in #1043
• [external-ci] point SPHINCS+ job to formosa repo by @fdupress in #1036
• [chore] fix unused unfold warnings by @fdupress in #1042

Full Changelog: r2026.05...r2026.06