title: Ltac : optional arguments tactic
body: <p>I want to make a Ltac tactic in coq which would take either 1 or 3 arguments. I have read about <code>ltac_No_arg</code> in the <a href="http://gallium.inria.fr/~fpottier/ssphs/LibTactics.html" rel="nofollow noreferrer"><code>LibTactics</code></a> module but if I understood it correctly I would have to invoke my tactic with :</p>
  
  <pre><code>Coq &lt; mytactic arg_1 ltac_no_arg ltac_no_arg.
  </code></pre>
  
  <p>which is not very convenient.</p>
  
  <p>Is there any way to get a result like this ? :</p>
  
  <pre><code>Coq &lt; mytactic arg_1.
  
  Coq &lt; mytactic arg_1 arg_2 arg_3.
  </code></pre>