This is the short name of the contribution. It is
used as a unique identifier of your contribution, so we recommend you
to make it short but meaningfull, w.r.t. the content of your
It should contain only letters or digits, each word beginning with an
uppercase letter. Examples of good names are: FiringSquad or
FunctionsInZFC; examples of wrong names are
high_school_geometry or tortoiseharealgorithm.
a tar file containing all the files; a Makefile made with
coq_makefile - supplied with Coq - is highly
a list of other contributions which are necessary to compile
this one (they must be referred to by the name given in the
In order to
make your contribution available from the Coq web site, we
expect you to select a license that allows us to redistribute it
and to keep it compatible with the new versions of Coq. Some
hints on how to choose a licence are given here.