- Update to version 8.16.0.
  * The guard checker (see `Guarded`) now ensures strong
    normalization under any reduction strategy.
  * Irrelevant terms (in the `SProp` sort) are now squashed to a
    dummy value during conversion, fixing a subject reduction 
    issue and making proof conversion faster.
  * Introduction of reversible coercions, which allow coercions 
    relying on meta-level resolution such as type-classes or 
    canonical structures. Also allow coercions that do not fullfill
    the uniform inheritance condition.
  * Generalized rewriting support for rewriting with `Type`-valued 
    relations and in `Type` contexts, using the
    `Classes.CMorphisms` library.
  * Added the boolean equality scheme command for decidable 
    inductive types.
  * Added a `Print Notation` command.
  * Incompatibilities in name generation for Program obligations,
    `eauto` treatment of tactic failure levels, use of `ident` in
    notations, parsing of module expressions.
  * Standard library reorganization and deprecations.
  * Improve the treatment of standard library numbers by
    `Extraction`.
- Coq requires ocamlfind at runtime now.

• Files Changed
• Browse Source