I'm adding some glue in Coq-Elpi to let one use tactics written in Elpi in the middle of terms. It is working quite nice, but I've a problem with "shelved goals". Elpi tactics return the list of subgoals and shelved goals, so I have the choice of what to do when the tac-in-term leaves goals open.

But I get a wrong behavior, namely the leftover goal, no matter how I declare it, gets duplicate when I call Unshelve.

```
Goal bool * bool.
epose ( X := (true , ltac:(shelve) : bool) ).
Unshelve. (* works , 1 extra *)
exact X.
exact false. (* extra *)
Qed.
Goal forall T (a b : T), G.
Proof.
move=> T a b.
epose (A := A.pack T (_ : hasA T)). (* this hides ltac:(elpi mytac ...) *)
Unshelve. (* I have 3 goals now! G + "hasA T" twice *)
```

These are the last lines of my tactic, where `declared_goals`

and `shelved_goals`

come from the Elpi code, and I did check that they contain no duplicate (in my tests, only one list is non empy).

```
tclTHENLIST [
tclEVARS (S.get engine state).sigma;
tclSETGOALS @@ List.map Proofview.with_empty_state declared_goals;
Proofview.shelve_goals shelved_goals
]
```

@Pierre-Marie Pédrot help!

The whole shelving mess is a bit over my head unfortunately.

Hum, I think I found it, I've a duplicate evar on my side.

sorry for the noise

:shrug:

After Maxime's last PR, the mess is much smaller (I think it got in, but I might be wrong)

In the end, it all makes sense. I'll add a rechability check in Coq-Elpi, so that a spurious evar does not turn out to be a goal. The API on the Coq side is very picky, if there was a "garbage collector" it would have just dropped the extra one :-/

Last updated: Dec 06 2023 at 14:01 UTC