CHANGELOG.md

2.5.1 (June 24, 2021)

• Improvement of the GADTs support.

2.5.0 (March 30, 2021)

• Beginning of support of GADTs without axioms, thanks to a pull-request of @pedrotst formal-land#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.

2.0.0 (December 15, 2019)

• First public release financed by Nomadic Labs.