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: Feb 04 2023 at 03:30 UTC