The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> > Everything is clear, except for:
> > 
> >   Bound to class nat
> > 
> > clause. What does that mean? Does anybody know? What si "nat class"?
> 
> I assume this is the result of a `Bind Scope nat_scope with nat`, which
> essentially means that nat_scope is used automatically for parsing
> arguments of a function of type nat -> ....
> 
> Why this is called a "class", I have no idea.

It is called class in the sense of coercion classes, as described in
Sections 2.8 and 18.2 of the reference manual. This e.g. includes
FunClass bound to function_scope and SortClass bound to type_scope.

Note that this has nothing to do with "type classes". A clarification
of the terminology would probably be useful to prevent the confusion
(I opened issue #6159 for that purpose).

Best,

Hugo