Methods such as monadic_rewrite_symb_exec_r should warn that discharging side-conditions failed

[Xaphiosis]

The specific case is monadic_rewrite_symb_exec_r which will attempt to automatically discharge, for example, the no_fail side condition. When it works, this is great, but when it fails there is no sign except for an extra subgoal. For small examples this is fine also, but for large proofs (e.g. fastpath rewrite proof) it's hard to notice that this failed, leading to a surprise no_fail goal out of nowhere before the wp part of the proof.

Some questions here are:

• Should we warn? In the spirit of backwards reasoning, dealing with the side-conditions later makes sense, but it will usually be by providing a rule that could just as easily be provided to monadic_rewrite_symb_exec_r or placed in the [wp] set.
• How do we warn? We'd need some kind of warn_tac that's an alternative to whatever tactic we're trying to apply, and have it not get repeatedly get set off by backtracking.
• Which other methods/tactics do people know that have this "why didn't you warn me?!" property that this issue could apply to?