Is there a MetaCoq function that just quotes thecurrent global environment?
I would expect its type to be
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.
You get the environment by adding
Last updated: Nov 29 2023 at 05:01 UTC