The Coq mailing list

[xiang sen <xiangsen AT ustc.edu>]

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