The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Take a look at the coq reference manual;
here is an exerpt which may be of some help:

12.1.3  Complex notations

Notations can be made from arbitraly complex symbols. One can for
instance define prefix notations. Coq < Notation "~ x" := (not x) (at
level 75, right associativity).

One can also define notations for incomplete terms, with the hole
expected to be inferred at typing time. Coq < Notation "x = y" := (@eq
_ x y) (at level 70, no associativity).

One can define closed notations whose both sides are symbols. In this
case, the default precedence level for inner subexpression is 200. Coq
< Notation "( x , y )" := (@pair _ _ x y) (at level 0).

One can also define notations for binders.
Coq < Notation "{ x : A  |  P }" := (sig A (fun x => P)) (at level 0).

In the last case though, there is a conflict with the notation for type
casts. This last notation, as shown by the command Print Grammar constr
is at level 100. To avoid x : A being parsed as a type cast, it is
necessary to put x at a level below 100, typically 99. Hence, a correct
definition is Coq < Notation "{ x : A  |  P }" := (sig A (fun x => P))
(at level 0, x at level 99).

See the next section for more about factorization.