Skip to content

Releases: inria-cambium/m1-tan

Coq's Guard Checker in Coq 8.19

20 Aug 15:53
Compare
Choose a tag to compare

This guard checker implemented in Coq works with MetaCoq 1.3.2 and Coq 8.19. It implements the guard checker in Coq's kernel in the master branch, as recent as at the time of release (last commit: d6550d). Currently, it achieves full agreement with Coq's guard checker on Coq's guard checker test suite, except for slow reduction on some examples, which it didn't terminate within the time allowed.

Full Changelog: https://github.com/inria-cambium/m1-tan/commits/v1.0.0