What's Changed
- tests: do not re-run Missing.fst checks every time by @mtzguido in #4327
- Pulse: fix branch return-type refinement leak in if/match/while guards by @KimayaBedarkar in #4324
- Consolidate Pulse big-operators onto forall+; remove OnRange by @gebner in #4323
- Check Pulse decreases for concrete recursion by @nikswamy in #4329
- Pulse: short-circuit stateful && / || operands by @KimayaBedarkar in #4322
- FStar.Bijection: fix mk_bijection to only require ghost functions by @mtzguido in #4331
- Revert "Pulse: short-circuit stateful && / || operands" (#4322) by @KimayaBedarkar in #4332
- Adding Float32 and Float64 by @mtzguido in #4328
- Validate float literal extraction by @eluvane in #4333
- Pulse: allow inline calc by @mtzguido in #4334
- Pulse: remove some spurious rewrites by @mtzguido in #4339
- Bump version to 2026.06.28 by @dzomo in #4341
New Contributors
Full Changelog: v2026.06.21...v2026.06.28
Contributors
gebner, mtzguido, and 4 other contributors