The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a way to consistently combine multiple coq files into a single coq file, such that the output of coqing that file will be the same as if you had coqed the original one?

If the files are all in the same directory and don't have weird characters, then I can wrap the contents of each file in [Module <filename>. ... End <filename>.], and then shove them all in a single file so that there are no forward references, and remove and [Require]s of that module, and replace [Require Import] with [Import], and [Require Export] with [Export].  However, I have not figured out a good way to do this when files are in subdirectories, and they depend on each other in such a way that I cannot place all of the files in a single subdirectory sequentially with one another (because some depend on files in other subdirectories, which themselves depend on other files in this subdirectory), without errors about multiply named modules.

Can anyone help me figure out how to do this?

Thanks,

Jason