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: Feb 09 2023 at 02:02 UTC