goal display in continuous mode

[gares]

The current automatic refresh of the goal is bad in continuous mode.

example:

Goal forall H H1, bla.
intros H. | (* I see the goal with H in the context, and forall H1, bla below the bar. OK *)
intros H|. (* I move back to introduce a new one, the goal changes to the original one *)
intros H H1|. (* still the old goal *)
intros H H1.| (* finally I see the effect *)

So it seems the goal to be displayed in continuous mode is the one below the cursor, not the one of the previous sentence.

[Durbatuluk1701]

I believe this probably has to do with vscoq.proof.pointInterpretationMode, the behavior you are seeing seems to be from mode 0 / Cursor; and maybe you want 1 / NextCommand?

[gares]

Could be. In that case continuons mode should force the right setting, if possible gaying out the other setting to signal the user it makes no sense to thinker with it.

I'll try tomorrow if it is the case that I have the "wrong" setting.