Pierre Courtieu
Pierre Courtieu
Agreed. A "about" command would be better.
Yes let us merge this and if someone feels motivated to replace it by a About buffer, feel free.
I am all for it. Should we merge this now?
Actually as explained by @SkySkimmer there are reasons to kill coqtop. Requires are still not correctly unloaded. https://coq.zulipchat.com/#narrow/stream/304019-Proof-General-users/topic/Restarting.20ProofGeneral/near/442904710 Hence my suggestion is the opposite: since we need to kill coqtop...
It is reasonable to ask to see the message when using `proof-assert-next-command-interactive`. @hendriktews maybe we can just modify this function to put `Unset Silent.` and `Set Silent.` around the command?
Sadly this command can be issued (even repeatedly) while previous commands are still being processed (in which case it only extends the command queue). I even suspect some users use...
I think rocq having an option `Print Goal Spontaneously` that we could unset would solve most of our problems. @hendriktews what do you think?
The whole change we made was to ensure that the goal displayed in the goals buffer is accurate. For this we had to disable completely the spontaneous goal printing of...
@hendriktews I will fill the corresponding rocq issue.
> > > That would require a notion of "current messages" which doesn't make sense. > > > > > > In this formulation it does not make sense. However,...