The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hello,

I am trying to learn the Coq system for notations. When I write:


Notation "'total2'" := (@sigT) (at level 0): type_scope. 
Notation "'tpair'" := (@existT) (at level 0) : type_scope.


Definition pr21 (T:UU) (P:T -> UU) (z: total2 T P) : T := 
match z with 
tpair t x => t
end.  


Coq complains at the definition by saying "Constructor expected". What is 
wrong there?

Vladimir.