The Coq mailing list

[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
-------------------------