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