The Coq mailing list

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

Hi,

> 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.

Notations of the form

  Notation id := ...

define a qualified identifier (they correspond to "Syntactic
Definition" of the pre-V8 syntax). As such, they can be referred to
using a long name as shown in the following session.

  (...)
  
  Coq < Notation a0 := (X0 myelem).
  
  Coq < Locate a0.
  Notation Top.a0
  
  Coq < Check Top.a0.
  a0
       : A

so that the notation a0 should'nt clash in any context with the
variable a0.

However, while checking your example, I found a bug. For instance, in
the following modified example

 Set Implicit Arguments.
 Record elem(X:Set) : Set := mk_elem{X0 : X}.
 Variables (A:Set) (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 a0.
   Proof.
     intro a0.

you should see 

  1 subgoal
  
    a0 : A
    ============================
    eq a0 Top.a0

what you won't if you don't use the today update of Coq 8.0 (cvs
tag V8-0-bugfix)...

Regards,
  
Hugo Herbelin