Look into using the same uniform error messaging code
Long discussion about the design of Hint Extern If tac Then ... and possibly more
expressive variants:
We came to settle on keeping the Hint Extern If which allows to express one "global" cut on brothers
in the proof search tree + a reference to "self"/continue for solving subgoals with the right
options/depth/db etc. One can then use once for internal cuts if needed.