The Coq mailing list

[Patrice Chalin<chalin AT encs.concordia.ca>]

Hi,

Consider the following simple record definition (contained in, say, RecTest.v
with nothing else):

Record R : Type := {
 f1 : nat;
 f2 : nat
}.

This is accepted by Coq, but if I add

  Require Import Imp.

to the start of the file where Imp is the theory from B.Pierce et al.'s
Software Foundations
(http://www.cs.princeton.edu/courses/archive/fall09/cos441/sf/) then I get the
following error message:

  Error: The reference f2 was not found in the current environment.

Now I understand that f2 is effectively a "global" function and that there can
be name clashes, but the error message is complaining that "f2" is _not 
found_.
 In any case it doesn't matter what I name the second record component, I
always get the same error. How can it be that an import can cause such an 
error
to arise?

Thanks in advance,
Patrice