The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

On Tue, Aug 2, 2011 at 2:33 AM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> In inductive definitions, you have two kind of parameters; as I don't
> know their names, I will call them "dependents" and "non dependents";
> then dependents are right of the colon; the non dependents are left.

If anyone knows a standard term for distinguishing these, I would very
much like to know what it is.  Some source I've seen uses "parameters"
for those to the left of the colon and "indices" for those to the
right.

Mike