Fatal errors in Elpi tactic can be caught by tactic-in-term

[pi8027]

I'm unsure whether it is a bug in Rocq or Rocq-Elpi, or even this is the intended behavior. But, IMO, fatal errors should remain fatal. Here is an example:

From elpi Require Import elpi.

Elpi Tactic test.
Elpi Accumulate lp:{{
solve _ _ :- coq.error "fatal error".
}}.

Goal False.
Succeed exact (ltac:(elpi test)) || idtac.
Abort.

[pi8027]

In my actual use case, my Elpi tactic generates a proof of an equation, and I call it from Ltac code, which looks like:

have proof := ltac:(elpi ...);
rewrite [pat]proof

to pass the generated proof to rewrite.

Another way to implement it (while avoiding tactic-in-term) is to let my Elpi tactic store the generated proof in the context, but then, I think the problem is that we cannot pass the name proof (actually generated by the fresh tactic) to an Elpi tactic.

[SkySkimmer]

possibly related rocq-prover/rocq#21247

[pi8027]

I will check if the issue is still present in Rocq master (or 9.3).