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: May 19 2024 at 18:02 UTC