2.5.3

Various small improvements.

2.5.2

• various small changes

2.5.1

• Improvement of the GADTs support.

2.5.0

• beginning of support for the GADTs without axioms, thanks to the work of @pedrotst
• support of OCaml 4.12, thanks to @lthms

2.4.1

• add basic support for matching on existential types and try ... with;
• add the @coq_type_annotation attribute;
• remove existential types from the modules conversion (unless for first-class modules);
• upgrade Dune dependency to the version 2.8.

See this blog post for more details on the removal of the existential types for the modules.

2.4.0

• upgrade to OCaml 4.10;
• simplify the header of the generated files;
• move the install folder from OCaml to CoqOfOCaml;
• add new configuration options and attributes, namely:
  • renaming_type_constructor
  • operator_infix
  • constant_warning
  • first_class_module_signature_blacklist
  • @coq_mutual_as_notation

2.3.0

• new configuration options;
• inlining of anonymous sub-signatures;
• functors and signed modules defined with top-level definitions instead of local let;
• support for the monadic notation of OCaml.

See this blog post for more details on the changes on functors and anonymous sub-signatures.

2.2.1

• use a more standard Dune build command 📦

2.2.0

• add a configuration file 📜
• Coq is now an optional dependency 📦

2.1.0

Main changes:

• support of functors;
• all the values are in Set (using the -impredicative-set option and exitentials in Set for first-class modules);
• basic GADT support with axioms;

We can now import the full Tezos protocol (40.000 OCaml lines). Details of the changes in CHANGELOG.md.