The Coq mailing list

[vincent rahli <vincent.rahli AT gmail.com>]

Thanks.

On Mon, Jun 2, 2014 at 8:01 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

I do not think you can do it. Compilation of Coq files is thought to be done at the file level. You can play with implicit parameters to leverage that burden, but that is about all you can do. There can also be some trick like defining a context type CT (ie. a record of all the types you will need for your files), start each file with a section declaring a variable of type CT, and then to add a parameter to all functions using CT will be simply done by adding a field to CT. You can have a fine grained control by defining various context types. Not sure I am clear though.

For modules, I think it is normal to forbid them inside sections. At end of sections, all definitions must be generalized, that would make module signature a lot less obvious. The module could also be parameterized by an other one, but that would imply to be able to automatically name modules created at end of sections.

2014-06-01 15:06 GMT+02:00 vincent rahli <vincent.rahli AT gmail.com>:

Hi,

Here is my issue.  I want to add a parameter to a definition D.  Adding
that parameter means that I will have to thread it through many definitions
and lemmas spanning over several files.

Is there some simple way to do that that does not involve updating each
and every definition and lemma that depends on D?

For example, is there a way to get the effect of wrapping

  Section Foo. Variable Bar : Baz. ... End Section.

around a bunch of files?

BTW, while testing a few things, I realized that modules are not allowed

inside sections.  Why is that?

Thanks.

Vincent.

--
.../Sedrikov\...