I think https://github.com/MetaCoq/metacoq/pull/790 and https://github.com/MetaCoq/metacoq/pull/789 are ready for merge
(Also interested in feedback / what needs to be done to merge https://github.com/MetaCoq/metacoq/pull/792)
More PRs for review: https://github.com/MetaCoq/metacoq/pull/802 and https://github.com/MetaCoq/metacoq/pull/803 are relatively minor PRs adding some utility lemmas that I use in making normalization into a typeclass
Last updated: Sep 15 2024 at 13:02 UTC