The Coq mailing list

[<kennethadammiller AT gmail.com>]

So, after looking at the vector specification at
http://coq.inria.fr/distrib/V8.4beta/stdlib/Coq.Vectors.VectorDef.html#
I'm lost as to why t was used in place of vector. Why would the designers
choose t instead of vector?

Also, as part of an assignment, I have to model some C unions in Coq-I'm new
to Coq, so I was wondering what data type I would use to get this done.