2.3.0

CHANGES:

Added

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

Fixed

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

Changed

• Do not propose installation of Emacs mode via opam anymore as it can easily be installed from Emacs.