- Update to version 8.20.0. The most impactful changes are:
  * A mechanism to add user-defined rewrite rules to Coq's reduction
    mechanisms; see chapter "User-defined rewrite rules".
  * Support for primitive strings in terms.
  * Reduction of the bytecode segment size, which in turn means
    that `.vo` files might now be considerably smaller.
- Notable breaking changes:
  * Syntactic global references passed through the `using` clauses
    of `auto`-like tactics are now handled as plain references
    rather than interpreted terms. In particular, their typeclass
    arguments will not be inferred. In general, the previous
    behaviour can be emulated by replacing `auto using foo` with
    `pose proof foo; auto`.
  * Argument order for the Ltac2 combinators `List.fold_left2` and
    `List.fold_right2` changed to be the same as in OCaml.
  * Importing a module containing a mutable Ltac2 definition does
    not undo its mutations. Replace `Ltac2 mutable foo :=
    some_expr.` with `Ltac2 mutable foo := some_expr. Ltac2 Set foo
    := some_expr.` to recover the previous behaviour.
  * Some renaming in the standard library. Deprecations are
    provided for a smooth transition.
- For more details, see the change log in coq-doc.

• Files Changed
• Browse Source