The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

>If this doesn't match your expectation, I can prepare a sample.

Please do.

The relation is the setoid identity which is used in the Add Ring 
command (in this case [@eq T']). I'm only guessing at what the tactic 
does based on the experiment I posted.

Gaëtan Gilbert

On 17/07/2017 13:56, Soegtrop, Michael wrote:
> Dear Gaetan,
>
> > You can also  use a type alias.
> thanks, an interesting hint!
>
> > This works because ring uses the relation to figure out which structure 
> > should be
> > used.
> This I don't get. In my situation all relations are different (including eq) 
> and all relations in the term I present to ring are either from on or the 
> other ring structure, only the type is the same. Still the ring tactic 
> selects the wrong ring structure. So my impression is that ring only looks at 
> the type. If this doesn't match your expectation, I can prepare a sample. It 
> is also possible that I did a mistake here.
>
> Which relation do you think ring looks at? The equality relation? How about 
> ring_simplify then?
>
> Best regards,
>
> Michael
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928