Stream: MetaCoq

Topic: Quoting the current global environment


view this post on Zulip Pierre Vial (Sep 04 2020 at 09:47):

Hello,
Is there a MetaCoq function that just quotes thecurrent global environment?
I would expect its type to be global_env or global_env_ext

view this post on Zulip Théo Winterhalter (Sep 04 2020 at 11:50):

Hi,
I think you can only get the environment on which depends a definition, it would otherwise get too big, containing the whole standard library for starters.

view this post on Zulip Théo Winterhalter (Sep 04 2020 at 11:51):

You get the environment by adding Recursively after Quote.

view this post on Zulip Pierre Vial (Sep 04 2020 at 12:25):

Ok, thanks!


Last updated: Aug 11 2022 at 02:03 UTC