Skip to content

Verified Extraction 0.9.2 for Coq 8.19

Choose a tag to compare

View all tags
@mattam82 mattam82 released this 23 Jul 10:38
· 6 commits to coq-8.19 since this release
v0.9.2-8.19
a018fc8
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

This release of verified extraction is compatible with MetaCoq 1.3.2 for Coq 8.19. It uses a verified pass for reordering of constructors, allowing to map Coq's booleans to OCaml's booleans correctly, simplifying interoperability with existing OCaml code.

What's Changed

  • Reorder cstrs and unique ffi by @mattam82 in #30
  • Adapt reification to take into account extract inductive directives by @mattam82 in #31

Full Changelog: v0.9.1-8.19...v0.9.2-8.19

Contributors

mattam82
Assets 3
Loading