The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 13/04/2015 03:53, George Van Treeck wrote:
> I have run into a problem where Coq seems to arbitrarily stop 
> importing lemmas from a file.

What do you mean by "import"? Does Coq refuse to compile the lemma
(which seems to be implied by the error you describe) or does the error
arise at Require time?

> All the lemmas in the file have proofs. But, the last couple return
> the error message: Error: The reference ... was not found in the
> current environment. The coq reference manual doesn't say why this
> error might occur when importing lemmas.

Do you have a more precise excerpt of this code? If by "importing
lemmas" you mean actually compiling them, then this error means that the
term X (the one of the error) is not in your local environment. This can
have various causes.

1. Because it was not loaded by Coq through a "Require" command on the
library that contains it.

2. Because it was not imported (in the sense of the "Import" command,
probably not what you describe as "importing"), and thus you need to
qualify the name (try to use the Locate X command).

3. Because it is in another scope you closed (section, module, etc.)

If you give us more details, maybe we can help you.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature