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: Aug 11 2022 at 02:03 UTC