What's Changed
- Require a proof of
nonempty tyfor divergent top-level lets by @gebner in #4404 - Pulse: give match branches the negated conditions of all preceding pa… by @nikswamy in #4410
- Simplify effect system and SMT encoding by @gebner in #4378
- Proposal: hierarchical namespaces by @amosr in #4379
- Pulse: preserve divergent effects through locals by @KimayaBedarkar in #4419
- CI: replace prebuilt Docker image with a cached opam setup action by @gebner in #4416
- Pulse: requires on annotated conditionals, and their effect by @gebner in #4420
- Pulse: purify spec-level let-bindings before slprop splitting (fixes #4421) by @hei411 in #4422
- Fix divergent while-loop guard rejection in Pulse by @hei411 in #4433
- Normalize: separate memo cells for weak and strong normalization by @gebner in #4434
- Speed up dependency scanning by @gebner in #4436
- tests/extraction: cross-backend extraction test matrix by @gebner in #4414
- Bump version to 2026.08.16 by @dzomo in #4438
New Contributors
Full Changelog: v2026.08.09...v2026.08.16
Contributors
gebner, amosr, and 4 other contributors