A preview for an upcoming major release in preparation for several courses and tutorials.
This brings lots of improvements:
- two-phase type checking (towards disentangling type checking from checking of verification conditions), more robust wrt. inference of implicit arguments
- extraction to OCaml preserves the structure of let-bindings
- extraction now erases all pure unit functions, lemmas and ghost functions
- and many many more, see https://github.com/FStarLang/FStar/blob/v0.9.6.0-alpha1/CHANGES.md for more details.