The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

AUGER Cédric 
<Cedric.Auger AT lri.fr>
 writes:
>> Yes, this is what I was previously doing; unfortunately [Section]s are
>> incompatible with [Module]s, which I would like to start using.
>
> What do you mean with that? You can perfectly open a section inside a
> module (I am almost certain that you also can open a module inside a
> section, but that is not the problem here).

Actually you can't.  I find that quite puzzling!  Can anybody explain
why this restriction is in place?  Is there any chance it might be
removed?

  "One can have sections inside a module or a module type, but not a
   module or a module type inside a section"

    -- http://coq.inria.fr/refman/Reference-Manual004.html#toc16

I must use Sections because as far as I can tell they are the only way
to get the massive generalization ("all global objects defined in the
section are generalized with respect to all variables and local
definitions it depends on in the section") required for the PHOAS
representation I'm using.  Inserting the quantifiers by hand would be
a nightmare...

> About modules, I expect you to have good reason to use them, as in Coq,
> they are a lot less interesting as one can think at first glance.

I need some way of managing the namespace; my development now has far
too many identifiers and they are beginning to clash.  The Foo.(bar)
notation is quite nice and very useful, but it seems that modules are
the only way to get this notation.

I would also like to avoid being forced to break up my scripts into
multiple files (except where I choose to do so) simply to structure the
namespace.  The library mechanism is nice, but I wish it wasn't based on
which file a declaration resides in.

  - a