Raising the failure level of a coq tactic

Question

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 repeat, or to cause backtracking). These failures are usually raised at failure level 0.

Failures raised at higher level “escape” the surrounding try or repeat block, and are useful to signal unexpected failures.

What I am missing is a way to run a tactic tac 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 repeat does not terminate due to a Ltac programming error on my side.

Can I implement such a failure-raising-level higher-order tactic in Ltac?

Leonidas Lampropoulos Leonidas Lampropoulos · Accepted Answer · 2017-07-24T16:37:20

You can write a tactic to achieve that in Ocaml. I put that on GitHub here.

For example the following should raise an error instead of silently succeeding:

repeat (match goal with 
          | [ |- _ ] => 
            raise_error_level (assert (3 = 3) by idtac)
        end).

Raising the failure level of a coq tactic

2 Answers