package coq-of-ocaml

2.5.2 (January 25, 2022)

• Various small improvements.

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 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.

2.0.0 (December 15, 2019)

• First public release financed by Nomadic Labs.