tutorial: mention @ltacfail! (fix #501)

examples/tutorial_coq_elpi_tactic.v

@@ -403,6 +403,47 @@ Lemma test_print (P Q : Prop) (H : P -> Q) (p : P) : Q.
 print P, p, (H p). (* .in .messages *)
 Abort.
 
+(*|
+
+========
+Failure
+========
+
+The :builtin:`coq.error` aborts the execution of both
+Elpi and any enclosing LTac context. This failure cannot be catched
+by LTac.
+
+On the contrary the :builtin:`coq.ltac.fail` builtin can be used to
+abort the execution of Elpi code in such a way that LTac can catch it.
+This API takes an integer akin to LTac's fail depth together with
+the error message to be displayed to the user.
+
+Library functions of the `assert!` family call, by default, :builtin:`coq.error`.
+The flag `@ltacfail! N` can be set to alter this behavior and turn erros into
+calls to `coq.ltac.fail N`.
+
+|*)
+
+Elpi Tactic abort.
+Elpi Accumulate lp:{{
+  solve _ _ :- coq.error "uncatchable".
+}}.
+
+Goal True.
+Fail elpi abort || idtac.
+Abort.
+
+Elpi Tactic fail.
+Elpi Accumulate lp:{{
+  solve (goal _ _ _ _ [int N]) _ :- coq.ltac.fail N "catchable".
+}}.
+
+Goal True.
+elpi fail 0 || idtac.
+Fail elpi fail 1 || idtac.
+Abort.
+
+
 (*|
 
 ========

src/coq_elpi_arg_syntax.mlg

@@ -12,7 +12,6 @@ open Gramlib
 open Pcoq.Constr
 open Pcoq.Prim
 open Pvernac.Vernac_
-open Tacarg
 open Pltac
 
 module EA = Coq_elpi_arg_HOAS