The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

The following solution seems to work.
==========================
Definition mynot {A} (a b:A) := a <> b.
Lemma ...
repeat (match goal with [H: context[?a <> ?b] |- _] => fold (mynot a
b) in H end).match goal with [H: context [?a = ?b] |- _] => ...
end.unfold mynot in *.
==========================
Best,Gil

2011/12/24 Marko Malikoviæ 
<marko AT ffri.hr>:
> Greetings,
>
> can somebody explain me how can I match equality in context without
> involving negation of inequality.
> For example, here I am interested only for terms ?a = ?b without ?a <> ?b:
>
> match goal with
>    | id : context [?a = ?b] |- _ => ...
> ...
> end
>
> Namely, ?a <> ?b is interpreted as ~ ?a = ?b. Because it include ?a <> ?b
> in result of matching.
>
> Thanx a lot,
>
> Marko Malikoviæ
>
> -----------------------
> Dr. Sc. Marko Malikoviæ
> Filozofski fakultet
> Sveuèili¹te u Rijeci
> ---------------------
> Ph.D. Marko Malikoviæ
> Faculty of Humanities and Social Sciences
> University of Rijeka, Croatia
> -----------------------------
>Â marko AT ffri.hr
> http://www.ffri.hr/~marko
> -------------------------
>