Release 2.3.0
CHANGES:
- Export to Coq.
- (API) the rewrite engine can match on the constant `TYPE`.
- Automatic coercion insertion mechanism.
For example, the command `coerce_rule coerce Int Float $x ↪ FloatOfInt $x;`
can be used to instruct Lambdapi to automatically coerce integers to floats
using the function `FloatOfInt`.
- Generation of metavariables through the rewriting engine.
- Application of pattern variables in rewrite rules RHS in the Dedukti
export.
- Dedukti export: invalid Dedukti module name were not brace-quoted,
for instance, `#REQUIRE module-name.` could be exported, while `module-name`
is not recognised by Dedukti2. It is now exported as `#REQUIRE {|module-name|}`,
and symbols are exported as `{|module-name|}.foo`.
- HRS and XTC exports.
- Do not propose installation of Emacs mode via opam anymore as it can easily be installed from Emacs.