The Coq mailing list

[filou AT labri.fr]

Hi all,

I was wondering if there exists a tactic to simplify boolean
expressions in hypotheses, such as in a goal of the form

H: a && false && b = true
-------------------------
False

I've tried "contradict H;ring" but it seems that ring doesn't deal with
inequalities.

Thanks,
Vincent