The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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?

The culprit is the following notation to be found in file Imp.v:

  Notation "c1 ; c2" := (CSeq c1 c2) (at level 80, right associativity).

This conflicts with the notation for records so that 

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

is understood as

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

Try for instance,

  Parameter c:com -> Type.
  Coercion c:com >-> Sortclass.
  Parameter f2:com.
  Record R : Type := { f1:CSkip; f2:com }.

and it will define R with one field f1.

This is a serious drawback of the grammar extensibility. Nothing in
Coq prevents users to introduce conflicting grammar rules and
extensions have to be used with care. I agree that this one (about
";") is a particularly annoying one but I don't see a solution to work
around it.

Hugo Herbelin