formal-land/coq-of-ocaml 2.0.0

on GitHub

• remove effects inference (as a simplification);
• connect to Merlin to analyse OCaml projects;
• better error messages (report all errors and show code extract);
• generate some code even with errors (replace errors by dummy code);
• support .mli files;
• support first-class modules;
• support GADTs (naive translation, may not type-check in Coq);
• support mutually recursive types.

This new release was developed working at and thanks to NomadicLabs. I also thanks all the people who interacted with the project.