"Incorrect number of goals" error after shelving and unshelving

[Janno]

Description of the problem

So far I have only been able to trigger this when using subst.

Small Rocq / Coq file to reproduce the bug

Goal forall (b : bool) (Hb : b = false), exists P, P.
Proof.
  intros.
  unshelve refine (@ex_intro _ _ _ _).
  2: {
    subst.
    shelve.
  }
  Unshelve.
  Fail all: (lazymatch goal with |- ?g => idtac g end). (* Fails with "Error: Incorrect number of goals (expected 2 tactics, was given 3)." *)
  lazymatch goal with |- ?g => idtac end. (* does not seem to print anything. this could be correct because no single goal is focused? *)
  Succeed all: (lazymatch goal with |- ?g => idtac g end). (* Correctly outputs two goals *)

Version of Rocq / Coq where this bug occurs

8.20, 9.1, 9.2

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response