Can't go back in proofs, or display is wrong with Rocq 9.2

[tperami]

I was trying to upgrade to Rocq 9.2, and, even with PG main branch, I still can't have the process of going back in proofs be correct

If I have the following script:

Lemma test: 2+2=4.
cbn.

If I go past cbn, the goal becomes 4 = 4 as expected, but when I go back (proof-undo-last-successful-command), the display goal is still 4 = 4. However, if I now do idtac (before the cbn), the goal indeed reverts to 2 + 2 = 4. I need to go back and then do one step forward to see to correct goal at my point.

From looking at the logs (running in silent mode) doing BackTo n. then Show. Still prints the goal from before the BackTo command, so this might also be a pure Rocq bug. Doing idtac at that point, print the expected thing`

I got the same result when calling the repl by hand. Doing:

Welcome to Rocq 9.2

<prompt>Rocq < 1 || 0 < </prompt>Lemma test: 2 + 2 = 4.

<prompt>test < 2 |test| 0 < </prompt>cbn.

<prompt>test < 3 |test| 0 < </prompt>Show.
1 goal (ID 3)
  
  ============================
  4 = 4

<prompt>test < 3 |test| 0 < </prompt>BackTo 2.

<prompt>test < 2 |test| 0 < </prompt>Show.
1 goal (ID 3)
  
  ============================
  4 = 4

<prompt>test < 2 |test| 0 < </prompt>idtac.

<prompt>test < 4 |test| 0 < </prompt>Show.
1 goal (ID 2)
  
  ============================
  2 + 2 = 4

<prompt>test < 4 |test| 0 < </prompt>

[tperami]

Maybe a solution is just to run idtac in front of Show. when in proof mode

[anton0xf]

It also reproduces with 9.0

[tperami]

Yes but I think in only appears in silent mode that only became the default for 9.2