The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Well... may be you are overstimating me :)
actuallly
> You've already done the hard work of figuring out which type family is
> matched with each of the different notations.
I does not even understand what this sentence can mean.... i'm trying
to understand
http://www.lix.polytechnique.fr/coq/stdlib/Coq.Init.Specif.html

Following you advice I was able to write
Definition ex1:= ((exist (@NoDup nat) (@nil nat) (NoDup_nil
nat)):{x:list nat | NoDup x}).
That again does not type since it is something of tipe ( sig NoDup ),
that for what I was able to understand should be the same of {x:list
nat | NoDup x}, but it seams not...

Moreover, i have noticed some Type insted of Prop in the declaration
of sigT, but while i can imagine lots of uses for sig
(list long at list n, and so on...), I cant figure usages for sigT :-(