From b749a0121f11deea0e53ce03c728cf3e07c16679 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 29 Sep 2023 17:28:21 +0200
Subject: [PATCH 1/2] tutorial: mention @ltacfail! (fix #501)

---
 examples/tutorial_coq_elpi_tactic.v | 41 +++++++++++++++++++++++++++++
 src/coq_elpi_arg_syntax.mlg         |  1 -
 2 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v
index e95cccf9d..5ad4681e3 100644
--- a/examples/tutorial_coq_elpi_tactic.v
+++ b/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.
+
+
 (*|
 
 ========
diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg
index 98e0855b6..d7b54a2f4 100644
--- a/src/coq_elpi_arg_syntax.mlg
+++ b/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

From 7eb7e0dada983af84e38ab8b9000b4f01e739305 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Sat, 30 Sep 2023 16:14:25 +0200
Subject: [PATCH 2/2] fix evar count

---
 examples/tutorial_coq_elpi_tactic.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v
index 5ad4681e3..ec1e31767 100644
--- a/examples/tutorial_coq_elpi_tactic.v
+++ b/examples/tutorial_coq_elpi_tactic.v
@@ -685,13 +685,13 @@ The set of constraints on `evar` represents the Coq data structure called
 sigma (sometimes also called evd or evar_map) that is used to
 represent the proof state in Coq. It is printed just afterwards:
  
-.. mquote:: .s(elpi show_more).msg{EVARS:*[?]X55*x + 1 = 0*}
+.. mquote:: .s(elpi show_more).msg{EVARS:*[?]X57*x + 1 = 0*}
    :language: text
 
-.. mquote:: .s(elpi show_more).msg{Coq-Elpi mapping:*RAW:*[?]X55 <-> *X1*ELAB:*[?]X55 <-> *X0*}
+.. mquote:: .s(elpi show_more).msg{Coq-Elpi mapping:*RAW:*[?]X57 <-> *X1*ELAB:*[?]X57 <-> *X0*}
    :language: text
 
-Here `?X55` is a Coq evar linked with Elpi's :e:`X0` and :e:`X1`.
+Here `?X57` is a Coq evar linked with Elpi's :e:`X0` and :e:`X1`.
 :e:`X1` represents the goal (the trigger) while :e:`X0` represent the proof.
 The meaning of the :e:`evar` Elpi predicate linking the two is that the term
 assigned to the trigger :e:`X1` has to be elaborated to the final proof term