Stream: MetaCoq

Topic: ✔ `cored` and `extends_decls`


view this post on Zulip Théo Winterhalter (Dec 08 2022 at 09:05):

Oh you need it there? Then I guess we must accept it. :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jason Gross (Dec 08 2022 at 09:29):

Thank you!

view this post on Zulip 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