Restore the error-handling behavior of [change], which was silently failing
when conversion in the goal failed.
Restrict eta-conversion to inductive records, fixing bug #3310.
Fix non-printing of coercions for primitive projections (fixes bug #3433).
Fix program using an the unsubstituted type of the original obligation
instead of the normalized one at the end of the proof. Fixes bug #3517.
Remove confusing behavior of unify_with_subterm that could fail with
NoOccurenceFound when only typeclass resolution failed. Might break
some scripts relying on backtracking on typeclass resolution failures
to find other terms to rewrite, which can be fixed using occurrences
or directly setoid_rewrite.