The Coq mailing list

[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.