The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Adam,

Yes, you are right! My oversight! The term ~foo will not (during pattern
matching) involve inequality. In fact, your and Chung-Kil's suggestions
are very similar.

Thanks again,

Marko Malikoviæ

> On 12/24/2011 02:28 PM, Marko Malikoviæ wrote:
>> The second solution does not fit to me because if I put "foo" instead of
>> all occurences of a = b then I can have foo and ~foo in the same
>> hypothesis.
>>
>
> Glad to hear that Chung-Kil's suggestion works.  I don't see the problem
> with using a named context, because such a context only has a single
> hole to be filled, even if the term initially found in that position
> appears multiple times in the goal.  Filling the hole will only put
> [foo] in that single position.
>


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