Ring tactic

[Bas Spitters]

Some parts of this message have been removed. Learn more about Nabble's security policy.

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