Théo Winterhalter (Dec 08 2022 at 09:05): Théo Winterhalter (Dec 08 2022 at 09:05):Oh you need it there? Then I guess we must accept it. :)
Jason Gross (Dec 08 2022 at 09:23):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.
Théo Winterhalter (Dec 08 2022 at 09:26):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.
Jason Gross (Dec 08 2022 at 09:29):Thank you!
Notification Bot (Dec 08 2022 at 09:29):Jason Gross has marked this topic as resolved.
Last updated: Feb 04 2023 at 01:03 UTC