The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT sophia.inria.fr>]

I have been a bit disturbed by the following behaviour of Notation : a name 
used
as a Notation does not become reserved even for the time the current section
being opened. This can lead to some confusions, for example, after:
----
Set Implicit Arguments.

Record elem(X:Set) : Set := mk_elem{X0 : X}.

Variable A:Set.

Variable myelem : elem A.

Inductive eq : A -> A -> Prop :=
  |refl : forall a:A, eq a a.

Notation a0 := (X0 myelem).

Lemma test : forall a :A, eq a a -> eq a a.
  Proof.
    intros.
    elim H.

----
the situation is:

  a : A
  H : eq a a
  ============================
   forall a0 : A, eq a0 a0



where a0 is supposed to be a fresh name.

Of course all this is not so harmful. Problems can be avoided by changing 
names
of the bounded variables in eq 's constructors (or by using inversion.. as..,
or by chosing an other notation...). Anyway, I would have expected Notation to
behave like Variable for names matters. Is there a reason why this difference?

Thanks in advance,

Assia Mahboubi

------------------------------------------------------
This message was sent using IMP: http://horde.org/imp/