Aaron Puchert fedf51e717 - Update to version 8.20.1. ...

* Fixed possible guard checker anomaly on fixpoints containing an
    inner fixpoint that is reducible (because of its main argument
    reducing to a constructor). This was a regression in 8.20.
  * Fixed spurious warnings about incompatible prefixes in presence
    of `as pattern syntax_modifier` or recursive notations.
  * Fixed a regression in `Hint Extern` matching primitive
    projections.

OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=69

2025-01-18 15:17:54 +00:00

33 KiB

Raw Permalink Blame History

View Raw