Release notes for F* 0.9.5

• Lean-inspired tactic framework (Nik, Victor, Jonathan, Guido, Kenji, et al -- WIP)
• Better reasoning by monadic reification, including for relational verification (Kenji et al)
• Much better pretty printer for inner syntax, particularly for error messages (Qunyan, Kenji, Nik, Jonathan, Samin)
• Serious improvements to interactive mode: including showing the types of things, jumping to definition, and auto-complete (Clement, Nik, et al)
• Constructive implementations of F*'s memory models replacing axiomatic ones (Aseem, Danel, et al)
• Support for extracting user-defined effects (Victor, Kenji, et al)
• Better support for interfaces in interactive mode
• Prettier OCaml extracted code (Victor, #857)
• More reproducible unsat cores (Christoph and Nik)
• Improved normalizer (Guido, Nik, et al)
• F* version bootstrapped in F# trailing less behind (Christoph, e.g. #871)
• Encoding of SMT lemmas involving recursive functions no longer introduce matching loops in SMT (#1028)
• Support for structs in generated low-level C code (Tahina)
• Split prims into prims and pervasives (Aseem)
• Brought back support for parallel processing using the --n_cores flag (Tomer and Christoph, #146 and #846)
• Edition of .fs files as F* files (Clement)

Upcomming :

• Indexed effects (Nik, Kenji -- WIP)