cannot step back across `phoare` lemmas

[oskgo]

MRE:

require import Real.

module M = {proc p()={}}.

phoare p: [M.p: true ==> true] = 1%r.
proof. proc; auto. qed.

Stepping back after stepping over qed does not work, requiring a full restart.

Curiously, the following variation works:

require import Real.

module M = {proc p()={}}.

phoare p: [M.p: true ==> true] = 1%r by proc; auto.

The workaround is to use lemma p: phoare[M.p: true ==> true] = 1%r instead.

[fdupress]

I think this is a proof-general keyword problem, similar to another we ran into recently? We need a way to feed keyword lists to PG, but I'm worried that our new rapid release cycle is going to interfere badly with theirs, which is... somewhat slower?

[oskgo]

I don't think that one issue and some missing syntax highlighting is worth creating schedule to sync with PG over. I think we can get away with fixing this once (by updating PG), being more careful about adding lemma kinds in the future and reassessing if something like this happens again.

[strub]

The keywords phoare (and certainly ehoare) should be added here:

https://github.com/ProofGeneral/PG/blob/649f8f0f1df614c96802e022b0ce0fbaeba6e4bf/easycrypt/easycrypt-syntax.el#L24