F* v2025.03.25

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 t to ?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