The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[Variable] in a module now means [Local Parameter]; change [Variable] to [Parameter] or [Axiom] when not in a section, and you should be fine.

-Jason

On Mar 20, 2015 11:44 AM, "Frederic Chyzak" <frederic.chyzak AT inria.fr> wrote:

Hi,

In the example described below, I get with 8.5beta1 a different
behaviour (in terms of the qualification needed) for different members
of an imported file.  This was not so in 8.4.  Is the present behaviour
expected, and if so, why?

Starting with ok.v (attached), all is OK: I can access M1.f exactly like
I do M2.f.

If I now move part of ok.v (the definition of both modules) to aux.v,
then require-import them into pb.v, I can no longer access M1.f
directly, and need to say aux.M1.f, in contrast with M2.f.  I would not
have expected that.

(For what is worth, I observed this with a freshly compiled 8.5beta1,
obtained via opam from git://github.com/coq/coq#V8.5beta1.)

Best regards,
Frédéric