What's Changed
- Respect extract_as for recursive definitions too by @mtzguido in #3776
- Perf fixes by @mtzguido in #3777
- Update fstar.opam to correspond to ocaml/opam-repository/packages/fstar by @chandradeepdey in #3779
- Fix a scoping bug for dependent matches in Tactics.check_match_complete by @mtzguido in #3780
- Tactics: return proper errors when guards fail for typing reflection by @mtzguido in #3781
- Tc: unconditionally restore options before encoding a module by @mtzguido in #3783
- Add missing apt-get update by @gebner in #3785
- Simplify
reveal ?u =?= reveal tto?u =?= hide (reveal t). by @gebner in #3784 - Parser: allow operators in restricted opens by @mtzguido in #3786
- Tc: proper ranges for spliced definitions by @mtzguido in #3787
- Prims.ml: remove mentions of lex_t/LexNil/LexCons by @mtzguido in #3788
- Tc: no need to refresh the solver when loading from cache by @mtzguido in #3789
- Tc: tweak error range for wrong universe instatiation by @mtzguido in #3790
- INSTALL.md: fix location of get_fstar_z3.sh by @mtzguido in #3791
- Revert a block and recheck it, if the push kind changes (i.e., allows… by @nikswamy in #3792
- Parser: fix parsing of (-) by @mtzguido in #3793
- Parser: mark lidentOrOperator as public by @mtzguido in #3794
- Tactics.NamedView: guaranteeing that pack does not change top-level ctor by @mtzguido in #3795
- Add a test by @mtzguido in #3796
- Extraction: nit, rename type to avoid pun with FStar.Syntax by @mtzguido in #3798
- add starmalloc to check-world by @mtzguido in #3799
- Reflection.Typing: add a knob for instantiate_implicits by @mtzguido in #3801
- Misc fixes by @mtzguido in #3803
- Error improvements, misc fixes by @mtzguido in #3805
- Improve error range for incoherent matches by @mtzguido in #3806
- Error nits by @mtzguido in #3807
- Misc improvements by @mtzguido in #3808
- Primops.Real: more simplifications by @mtzguido in #3809
- Bump version number by @mtzguido in #3811
Full Changelog: v2025.02.17...v2025.03.25