The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

This looks like a regression. You should report a bug at
https://github.com/coq/coq/issues.

Best,

Hugo Herbelin

On Fri, Nov 17, 2017 at 03:56:22PM +0200, Ilmārs Cīrulis wrote:
> (The version is the latest - Coq 8.7.0.)
> 
> On Fri, Nov 17, 2017 at 3:54 PM, Ilmārs Cīrulis 
> <ilmars.cirulis AT gmail.com>
> wrote:
> 
>     Hello. 
> 
> 
> 
>         Require Import Omega ArithRing. 
> 
>          
> 
>         Goal (2+2=4).
>         Proof.
>           ring_simplify (2+2).
>           try omega. compute. omega.
>         Qed.
> 
> 
>     Tactic ring_simplify results in such goal:
> 
>         N.to_nat 4 = 4
> 
> 
>     I included omega tactic to show, how this change could break older 
> proofs.
>     For example, it actually broke my tiny proof of "forall n m, 2 * n * n 
> = m
>     * m -> m = 0", that I accidentally revisited.
> 
>     Best regards,
>     Ilmars
> 
>