I want to make a Ltac tactic in coq which would take either 1 or 3 arguments. I have read about ltac_No_arg in the LibTactics module but if I understood it correctly I would have to invoke my tactic with :
Coq < mytactic arg_1 ltac_no_arg ltac_no_arg.
which is not very convenient.
Is there any way to get a result like this ? :
Coq < mytactic arg_1.
Coq < mytactic arg_1 arg_2 arg_3.