The Coq mailing list

[Gregory Bush <gbush AT mysck.com>]

In the following example, is there a modifier I can use when declaring  
the notation so it doesn't hide the notation for sigT?

Require Import List.

(* So far so good *)

Check {x : nat & {y | x < y}}.

Notation "{ A , .. , B }" := (cons A .. (cons B nil) ..).

(* Oops *)

Check {x : nat & {y | x < y}}.