The Coq mailing list

[anoun AT labri.fr]

Hi Sen,
Your tactic works if you use the type 'ex' instead of its notation (exists 
_:_,
)

Ltac splitex :=
repeat match goal with
 | H : ex _ |- _ => inversion_clear H
 end.

(*very simple example*)

Require Omega.
Lemma ex_try:forall m,(exists n:nat, n<m)->(exists n:nat,n+2<m)->m>=3.
intros.
splitex.
omega.
Qed.


Houda

> Hi , everyone :
>
> I used below to define a tactic :
>
> Ltac splitex :=
> repeat match goal with
> | H : exists _:_, _ |- _ => inversion_clear H
> end.
>
> But it does not work. Coqtop reports :
> Syntax error: [constr:ident] expected after 'exists' (in
> [constr:binder_constr]
>
> All the best!
> Sen
> --------------------------------------------------------
> 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
>




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.