The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Hi, I'm defining some tactiques and I'm tring to obtain a nice sintax.
If i make
Check a b c.
coq interpret it as Check (a b c).
but i i make apply a b c.
coq interpret it as (apply a) b c.
is there any way i can use to define Check like tactiques?
Thanks.
Marco.