Beginning of support of GADTs without axioms, thanks to a pull-request of @pedrotst https://github.com/clarus/coq-of-ocaml/pull/166.
Upgrade OCaml to the version 4.12, thanks to @lthms.
2.4.1 (March 15, 2021)
Add basic translation of try ... with with extensible types (cannot run in Coq but may be extracted to OCaml).
Add basic support for matching on extensible types.
Add the attribute @coq_type_annotation to generate the type annotation of an expression.
Show nicer error messages for errors in the configuration file.
Remove existential types from the modules (except for the first-class modules).
Upgrade OCaml to the version 4.10.
Upgrade Dune to the version 2.8.
2.4.0 (January 11, 2021)
Install the Coq proofs in CoqOfOCaml rather than OCaml for clarity.
Simpler header at the top of the generated files.
Try to import documentation comments from OCaml.
Do not ignore sequences of instructions anymore.
Add support for top-level definitions as init_module functions.
Add the attribute @coq_mutual_as_notation to translate a mutually recursive function as a notation.
Add the configuration option renaming_type_constructor to rename some type constructors.
Add the configuration option operator_infix to have notations for the infix operators.
Add the configuration option constant_warning to disable warnings when converting constants.
Add the configuration option first_class_module_signature_blacklist to ignore some signatures in the search of a signature name.
2.3.0 (November 3, 2020)
Add support for the OCaml's monadic notation.
Add support for records with polymorphic fields.
Add the attribute @coq_cast to force an unsafe cast of a sub-expression.
Rename the attribute @coq_axiom as @coq_axiom_with_reason.
Add the attribute @coq_precise_signature to help to distinguish between ambiguous signatures.
Remove the generation of Import in Coq and expand the names regardless of the open commands, in order to be compatible with local opens.
Add support for anonymous sub-signatures.
Generate functors using a type class of the current arguments.
Add the configuration option merge_returns.
Add the configuration option merge_types.
Add the configuration options monadic_lets (renaming of monadic_bind), monadic_let_returns, monadic_rets and monadic_ret_lets.
Add a @coq_plain_module attribute to force a module to be compiled as a plain module.
Add the configuration option renaming_rules.
Add support for generative functors (using functors with a unit parameter).
Add a mandatory string parameter to the @coq_axiom attribute in order to give a reason for the axiom.
2.2.1 (June 19, 2020)
Use a more standard Dune build command by keeping in the source the parser generated by Menhir.
2.2.0 (June 17, 2020)
Ignore unreachable expressions in match cases.
Add configuration to black list errors containing a certain message.
Add configuration to disable exit with error code on some files.
Exit with a non-null code in case of error.
Add configuration for the requires from long ident.
Add configuration to find the type of a polymorphic variant.
Add configuration to blacklist some errors.
Add configuration to blacklist some first-class module paths.
Add configuration to rename some variants.
Add configuration to rename some constructors.
Add configuration for module barriers in record aliases.
Add configuration to escape some value names.
Add configuration to add head suffix in the generated file.
Add configuration to add monadic operators.
Add configuration to specify dependencies required as mli files.
Add configuration to list the required files in a file, together with an import or not.
Add configuration to disable guard or positivity checking.
Add handling of a configuration file.
Add the @coq_phantom attribute to force an abstract type declaration to be phantom.
2.1.0 (March 20, 2020)
Add automatic re-ordering of type synonyms in mutual types to generate valid definitions.
Add minimal handling of class types as records.
Ignore type parameters with constraints (like being a sub-type of some variants).
Add a @coq_struct "param" attribute to specify the decreasing parameter name of fixpoints.
Add a tactic rewrite_cast_exists_eval_eq to simplify the use of the cast_exists axiom in proofs.
Name the arguments of the signatures.
Rename obj_magic as cast.
Set the primitive projection flag.
Add support for the with operator on constructor records.
Add an attribute @coq_match_gadt_with_result for GADT matches with casts for the results.
Do not generate casts for the return values of the match branches with @coq_match_gadt.
Remove the rarely used match exception when false construct for default return value in matches.
Add arity annotations for the existentials.
Eliminate phantom types and propagate this erasing.
Inline the application operators @@ and |>.
Put first-class modules in Set, using existentials in impredicative sets.
Add a @coq_match_with_default to generate a default branch for incomplete matches.
Add a @coq_force_gadt attribute to force a type to be defined as a GADT (without type parameters).
Add basic handling of module alias and typeof in .mli files.
Add more type annotations on values to better support polymorphic values.
Add better support for include of signatures in .mli files.
Add support of open in .mli files.
Upgrade to Coq 8.11.
Add support for functors inside signatures.
Add a special treatment with no axioms for the matching of algebraic types with existentials which are not GADTs (with the same type parameters for all the constructors).
Add an annotation mechanism for implicits for Coq.
Generate the JSON output in a default file.
Optimize the execution time to find the name of a signature.
Name the type of the records of constructors.
Add an annotation mechanism to generate axioms for the match of GADTs.
Use record.(field) to access record fields.
Add an axiom for assert.
Add basic support for includes of module types with sub-modules.
Add with notation for records.
Ignore patterns with extensible types.
Replace the generation of Export by Include (fix).
Add support of include in first-class module values.
Add support of functor definitions.
Add an annotation mechanism [@axiom] to ignore the content of some definitions.
Use list notation for list values.
Add support for when clauses in match.
Disable recursivity checks in Coq.
Change the include of signature to preserve the first-class sub-modules.
Define a default value for the extensible types.
Add support for constructors using records as parameters.
Add polymorphic record fields for modules with polymorphic elements.
Compute the shape of a module by only looking at the top-level of definitions.
Add support of functor application.
Use let to represent intermediate results in the definition of a first-class module value.
Define modules with a named signature as dependent records.
Add changelog file.
Add support for include of modules represented as a record.
Fix bug on ambiguous detection of first-class module signatures.
Ignore top-level let () = ... and the left-hand side of expression sequences ... ; ....
Capitalize generated file names.
Add the notation record.[field] to access to records with existential types.
Use tuples with primitive projections for the tuples of existential types in first-class modules (notation [x, y, z] for the values, [X * Y * Z] for the types).
Only use the value names to infer a module type name to handle destructive type substitutions (:= operator).
Add support for functor declarations.
Handle include in signatures of .mli files.
Wrap records into modules to prevent name collisions with projections.
Add support for polymorphic abstract types in modules.
Put more generated errors as comments to allow partial compilation.
Add support for module declarations with an anonymous signature in .mli files (by unfolding the signature).
Add support for module type definitions in .mli files.
Generate inductive type definitions for type definitions as polymorphic variants.
Convert inlined polymorphic variant types to sum types with annotations in comments.
Have a mechanism to lift some value names independently of type names to prevent name collisions.
Use Set instead of Type (may require to use the -impredicative-set flag to compile generated files).
Reduce the number of parenthesis in generated types using the precedence of the type operators.