The Coq mailing list

[Romain Janvier <Romain.Janvier AT imag.fr>]

I want to write something like that in a tactic:

Tactic Definition tac:=
Match Context With
...
|[id: (EX ?1| ?2)|-?3] -> Induction id
...


Want I give that to Coq, it thinks that the "|" after EX means that I'm 
trying to describe another case.

So How can I do to write a tactic that eliminate EX in the hypothesis?