Goal which is both shelved and displayed

[ckeller]

Hi
I observe the following behavior:

From elpi Require Import elpi.

Elpi Tactic dummy.
Elpi Accumulate lp:{{ solve _ _. }}.

Goal O = O /\ O = O.
  split.
  elpi dummy.    (* Here the proof state shows 2 focused goals and 1 shelved goal *)
  Unshelve.      (* Here the proof state shows the same 2 focused goals
                    and the shelved goal has been removed *)
Abort.

Thanks!

[ckeller]

@gares Thanks for the quick fix!
I was about to post this additionnal comment: if I use unshelve to bypass this bug, I observe a strange behavior in combination with Ltac2:

From elpi Require Import elpi.

Elpi Tactic elpi_split.
Elpi Accumulate lp:{{
  solve G GS :-
    coq.ltac.call "split" [] G GS.
}}.

From Ltac2 Require Import Ltac2 Printf.
Set Default Proof Mode "Classic".

Ltac2 test_numgoals_split () :=
  Control.enter (fun () =>
    printf "numgoals before split = %i" (Control.numgoals ());
    ltac1:(unshelve split);
    printf "numgoals after split = %i" (Control.numgoals ())
  ).

Ltac2 test_numgoals_elpi_split () :=
  Control.enter (fun () =>
    printf "numgoals before split = %i" (Control.numgoals ());
    ltac1:(unshelve elpi elpi_split);
    printf "numgoals after split = %i" (Control.numgoals ())
  ).

Goal (0 = 0 /\ 1 = 1) /\ 2 = 2.
  split.
  ltac2:(test_numgoals_split ()). (* before: 1 ; after: 2, as expected *)
Abort.

Goal (0 = 0 /\ 1 = 1) /\ 2 = 2.
  split.
  ltac2:(test_numgoals_elpi_split ()). (* before: 1 ; after: 3! *)
Abort.

Maybe you want to test it with your patch?