Commit 2023-11-19 20:53 693fd795View on Github →
exact_mod_cast tactic with
mod_cast elaborator where possible (#8404)
We still have the
exact_mod_cast tactic, used in a few places, which somehow (?) works a little bit harder to prevent the expected type influencing the elaboration of the term. I would like to get to the bottom of this, and it will be easier once the only usages of
exact_mod_cast are the ones that don't work using the term elaborator by itself.