The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Consider the following code:


Variable T:Type.
Variable P:T ->  Type.

Structure TP: Type := {pr1:>T ; pr2:P pr1}.

Variable  X:TP.

Canonical Structure X.

Coq complains that  "Error: X is not a structure object.". What is then a 
"structure object"?

Thanks!
Vladimir.