Minimize final proof script

[JasonGross]

Indeed the minimizer is not great at minimizing errors which occur in the middle or towards the end of long proof scripts. Perhaps I should add a pass which, when the error is due to a proof script, attempts to replace the goal with an equivalent one generated by doing repeat match goal with H : _ |- _ => idtac H; revert H end. Set Printing All. Abort. Goal <printed goal>. intros <hyps>. <rest of the proof script>. and see if that generates an equivalent error. I guess I should also set evars in an attempt to mimic the goal more closely. And I guess we should default to doing this pass (always?), and add --no-minimize-final-proof-script to disable it.

Thanks for tagging me @Alizter !

Originally posted by @JasonGross in coq/coq#15517 (comment)