The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I don't currently use coqdep to get the dependencies, though I might do that in the future.  The problem that I'm trying to solve currently, though, is not figuring out the dependency chain (or a topological sort thereof), but inlining all of the code into a single file without running into name clashes.

-Jason

On Thu, May 9, 2013 at 3:19 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:

Le Thu, 9 May 2013 14:17:41 -0400,
Jason Gross <jasongross9 AT gmail.com> a écrit :

> Hi,
> Thanks, but the intended output is a single stand-alone .v file,
> which I would then post-process.  I'm looking for a programmatic way
> to inline all of the non-stdlib dependencies of a .v file, as a first
> step in automatically minifying buggy code, to create a small test
> case.
>
> -Jason

Have you thought of using coqdep to get the dependencies? (I did not
really follow this thread, so maybe someone already talked of it.)