In know that some users don't care much about it, but if it is not too much work, it would be great to have soon. I am personally really using it day-to-day for tutorials, but also when I am working to easily compare how different tactics do different stuffs, or if I am writing a tactic to check it improves / does not regress etc...

So I understand your use cases. I am not sure what to do after the discussion in #687. @ybertot what is your take on this ?

Would could have a longer discussion on that, but I have the feeling they are different. Are they ? From what I understand from the discussion, reset changes the environment and parsing because of notation ? But isn't Restart simply restarting the proof ?

Note also this similar feature request that I would like: restart but for a bullet (you restart last time the goal has been focused with a bullet) https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Restart.20for.20bullet

Not sure how linked it is // how different / harder it is to implement

I like to use Restart when teaching Coq to students, where it is helpful to be able to show different ways of doing a proof -- or to show "see, here we are stuck, so let's start over again from scratch". I can work around that by using Abort. and repeating the lemma statement, but Restart. is a lot nicer.

Restart seems a lot less dangerous than Reset, so I don't quite see that this would have the same concerns as #687.

I agree with @RalfJung. I didn't even know Reset exists and I don't mind whether it is supported or not, but Restart is used in lots of teaching material for good reason. Removing Restart both makes teaching material worse and incurs the overhead of having to rewrite the teaching material so it stays compatible with vscoq2.

Would it be hard to get Restart back?