ring
is unusable in robust tactic automation
#12553
Labels
kind: design discussion
Discussion about the design of a feature.
part: ring/field
The ring and field tactics.
Description of the problem
Because
Add Ring
followsImport
rather thanExport
and because there seems to be no way to pass a ring structure to thering
tactic locally,ring
is unusable in automation that needs to be robust to reuse. Please add a variant ofring
that allows passing the ring structure, or a way to pick upring
structure from the context. (Why not just makeAdd Ring
register some typeclass instances?) (Presumably the same is true offield
.)Coq Version
8.11.0
The text was updated successfully, but these errors were encountered: