Warn on useless unfolds by default

[oskgo]

Removes the und_delta pragma, turning it on by default. Also fixes the stdlib to avoid emitting these new warnings.

I was a bit worried there might be false positives, but the worst I've seen is it emitting a warning for rewrite chains with multiple active goals when the unfold is useless in one of the goals. This was the case for the changes I made to RealSeries and BitEncoding. I think this is fair to keep around since we have the same behaviour for other rewrites when they fail on a single subgoal.

Do we want to merge this or #1014 first? The one that gets merged last will have to deal with the additional warnings from useless unfolds of auto unfolded operators.

[alleystoughton]

What the argument against making this an error not a warning? The problem with warnings is that unless one is single stepping in Proof General or running in batch mode, they'll be missed. Just as rewrite foo is an error if it can't be applied, why not make unfolding that does nothing an error?

[fdupress]

What the argument against making this an error not a warning? The problem with warnings is that unless one is single stepping in Proof General or running in batch mode, they'll be missed. Just as rewrite foo is an error if it can't be applied, why not make unfolding that does nothing an error?

"No breaking changes in the two weeks before a release if we can avoid it."

This gives us a nice bit of staging to detect breakage in external proofs without having to change them, so that the switch to making it an error is easier in the next release cycle.