Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."
(made push command with wrong local ref; leaving control to Matthieu
on new revert)

This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a.