The Coq mailing list

[jandronick <jandronick AT axalto.com>]

Hello,
Is their a way to exclude an hypothesis of the tactic intuition ?
I mean, if I have :
    H : A \/ B 
   -------------
   P1 /\ P2 /\ P3 /\ P4 /\ P5
and that I need to distinguish the case A of the case B only to prove P1, I 
would like to do something like "intuition except H" not to be obliged to 
prove P2, ..., P5 in the case A and prove again P2, ..., P5 for the case B...
I hope it is clear for someone... ;-)
June