Oh you need it there? Then I guess we must accept it. :)
PR at https://github.com/MetaCoq/metacoq/pull/801
The proof is needed because erasure needs normalization not just in the global environment it's passed, but also in the env that results from popping off decls.
I'm surprised because I thought cored would never appear in a setting where you change the global environment. Anyway we can merge it I guess.
Thank you!
Jason Gross has marked this topic as resolved.
Last updated: Feb 04 2023 at 01:03 UTC