The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Hai WAN wrote:
> What does it mean by "Declare Module f : F_sig.". Does it mean that we 
> declare a module f of signiture F_sig? Is it similar to "Variable f : 
> F_sig"?

I always thought of [Declare Module] as a command that only makes sense 
inside signatures.  I'm surprised that it's allowed inside a module 
definition; I certainly don't yet see a reason to use it that way.

> I then wrote the following codes, which make totally confused.
>
> ---------------------------------------------------
>
> Goal False.
> apply F_mod.ff.
> Qed.
>
> ---------------------------------------------------

In cases like this, you can always use [Print Assumptions] to see 
whether your proof really depends on some hidden axiom.  (In this case, 
it does.)

Theorem bad : False.
apply F_mod.ff.
Qed.

Print Assumptions bad.

(* Coq says: *)
Axioms:
F_mod.f.F : False