The Coq mailing list

[Frederic Chyzak <frederic.chyzak AT inria.fr>]

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

Module Type M1_sig.

Variable f : nat -> nat.

End M1_sig.

Module M1 : M1_sig.

Fixpoint f (n : nat) : nat := match n with
| O => S 0
| S m => match m with
    | O => S 0
    | S l => f m + f l
    end
end.

End M1.

Module M2.

Fixpoint f (n : nat) : nat := match n with
| O => S 0
| S m => match m with
    | O => S 0
    | S l => f m + f l
    end
end.

End M2.

Definition g (n : nat) : nat := n + n.

Module Type M1_sig.

Variable f : nat -> nat.

End M1_sig.

Module M1 : M1_sig.

Fixpoint f (n : nat) : nat := match n with
| O => S 0
| S m => match m with
    | O => S 0
    | S l => f m + f l
    end
end.

End M1.

Module M2.

Fixpoint f (n : nat) : nat := match n with
| O => S 0
| S m => match m with
    | O => S 0
    | S l => f m + f l
    end
end.

End M2.

Definition g (n : nat) : nat := n + n.


Eval compute in M1.f 5.
Eval compute in M2.f 5.
Eval compute in g 5.

Require Import aux.

(* Why is this "aux." qualification necessary? *)
Fail Eval compute in M1.f 5.
  (* The command has indeed failed with message:
     The reference M1.f was not found in the current environment. *)
Eval compute in aux.M1.f 5.

Eval compute in aux.M2.f 5.

(* But not here? *)
Eval compute in M2.f 5.
Eval compute in g 5.