The Coq mailing list

[Benjamin GREGOIRE <Benjamin.Gregoire AT inria.fr>]

Romain Janvier wrote:

> I want to write something like that in a tactic:
>
> Tactic Definition tac:=
> Match Context With
> ...
> |[id: (EX ?1| ?2)|-?3] -> Induction id
> ...

Try :
Tactic Definition tac:=
Match Context With
.....
| [id : (ex ?1 ?2) |- ?] -> 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?
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club