Open
Description
Currently it seems like the CertiCoq pipeline only works on a given global enviroment (given in full).
My strategy as thus been to do a BFS of the definition graph to fetch all required dependencies (and only those) and put them in a single compile environment.
I like the implementation, it's pretty sweet and short, but long term you'd want to generate multiple files that reflect the structure of the input Agda project.