The Coq mailing list

[xiang sen <xiangsen AT ustc.edu>]

Hi, all

I want to apply my customized tactic to a specified hypo.

So I do this:

Ltac reverse H :=
match goal with
| [ H : ? a < ?b |- _ ] => assert ( b > a); [ omega | clear H]
end.

I works well when there is only one hypo matching some x < y,
but if there are several hypo such as H1 : a < b, H2 : x < y,
"reverse H1" doesn't work as expected.

Why and how? Thanks

Best,
Xiang Sen