The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

I would like to do the following:
Add Ring polyring_th : poly_ring.
Or possibly:
Add Ring polyring_th (R:Ring): (poly_ring R).

However, I seem to need to register the polyring each time I introduce a new ring:

Variable R:Ring.
Add Ring polyring_th : (poly_ring R).

Am I missing something?

Thanks,

Bas