The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 08/09/2016 01:43 PM, Soegtrop, Michael wrote:
> But I think ring and ring_simplify have bugs. Applying ring_simplifiy on the 
> converted goal results in:
>
> eqmod 3 (addmod 3 0 x) (mulmod 3 1 x)

It is not a bug but a feature ;-)

the ring tactic does not know that 3 mod 3 = 0 but the reification 
does!! So the constant 3 is translated into 0 that is why you have this 
strange behavour.

--
Laurent