The Coq mailing list

[filou AT labri.fr]

Laurent Théry 
<Laurent.Thery AT sophia.inria.fr>
 a écrit :

> There is something wrong with your environment.
>
> ===
>
> Require Import Bool Ring.
>
> Goal forall a b, a && false && b = true -> True.
>
> intros.
> ring_simplify in H.
>
> =============
>
> works
>
> --
> Laurent

No, I just didn't know the ring_simplify tactic existed.
Thanks.

Vincent