Skip to content

1.0-beta2

Pre-release
Pre-release
Compare
Choose a tag to compare
@mattam82 mattam82 released this 21 Nov 15:34
v1.0-8.6-beta2
fa5263d
This commit was created on github.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
Learn about vigilant mode.

This second beta release includes one main new feature:

  • Support for mutual and nested structurally recursive definitions
    using top-level "with" and "where" keywords, including generation
    of the expected elimination principles.

It also fixes incompatibilities with various ocaml versions and external Coq
libraries (tested with ssreflect/mathcomp and coq-extlib).

Assets 2
Loading