title: Raising the failure level of a coq tactic
body: <p>When implementing a complex tactic in Ltac, there are some Ltac commands or tactic invocation that I expect to fail and where that is expected (e.g. to terminate a <code>repeat</code>, or to cause backtracking). These failures are usually raised at failure level 0.</p>
  
  <p>Failures raised at higher level “escape” the surrounding <code>try</code> or <code>repeat</code> block, and are useful to signal unexpected failures.</p>
  
  <p>What I am missing is a way to run a tactic <code>tac</code> and treat its failure, even at level 0, to be at a higher level, while retaining the message of the failure. This would let me make sure that <code>repeat</code> does not terminate due to a Ltac programming error on my side.</p>
  
  <p>Can I implement such a failure-raising-level higher-order tactic in Ltac?</p>