This is another big release with lots of changes and new features compared to v0.9.4.0

Main new features

• Proofs by reification (see this paper)
• A revision of the libraries based on a new formal account of monotonic state (see this paper)
• Extraction of programs with user-defined effects
• Experimental support for tactics
• New IDE protocol and new IDE features: autocompletion, evaluation, real-time syntax checking, jump-to-definition, type-at-point, etc.

Changes and other improvements

• A reorganization of the library and a single fstarlib.cmxa against which to link all F* programs compiled to OCaml (this change is incompatible with previous versions of F*)
• A new printer of source terms
• Revised error reporting from failed SMT queries
• Improved support for separate compilation via a binary format for checked modules
• Fixed a ton of bugs (179 closed GitHub issues)