The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Hi all

I am writing a tactic that looks for hypotheses of a certain shape

 | H : P x |- _
 | H : ~ P x |- _

and then I want it to introduce (depending on what it found) ~ P x and P x respectively. (P is just a place holder, I know it is generally not true that P x -> ~ P x)

I now have 2 questions

1) I want the hypotheses introduced by this tactic to be named not : _, not2 : _ , not2 : _ ...

Is this possible to do in ltac?

2) since the tactic introduces hypotheses of the same shape, is there a way to make sure that the tactic never matches on the generated hypotheses? 

Thanks in advance

Warm regards

Chris