The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Sylvie.Boldo AT inria.fr
 wrote:
> Hello,
>
> Many thanks Benjamin for the solution modifying ring !!
> It works great (and does not get out of sections). I never thought I 
> would ever modify ring...
Hello,
You have no idea of all the things you can modify in the new ring! In 
fact the only thing that is hardwired is the definition of the ring 
structure (and possibly one or two things from InitialRing.v). Then, all 
that is coded in ML is a tactic called ring_lookup that, given a list of 
terms, returns the appropriate ring structure and auxiliary tactics 
(constant, pre and post). All that is defined in Ring_polynom and 
Ring_tac could be duplicated and modified as you need, and define a new 
tactic ring2 that take advantage of all (past and future) Add Ring 
declarations.

Well, OK, for the moment, you have to dig in the guts of the tactic, and 
the code could probably be simpler, so you have to invest some time to 
achieve significant changes.

Regarding the ring_simplify tactic, I should warn you that it is a quite 
unstable tactic, and the spec of the normal forms changes quite often as 
Benjamin, Laurent (or I) code new features. ring is *much* more robust, 
and when possible you should really consider replacing ring_simplify by 
(replace <expr1> with <expr2> by ring). When expressions are big, using 
"match goal with ..." to extract large subterms of the goal can help.

Bruno.