This has the following advantages:
- We need fewer adhoc
Hint Externinstances for the proof mode, we can just use
- We can consistently use the
refineunification algorithm when trying to unify a hypothesis/conclusion of a lemma/wand to the goal. This is currently only done by
iAssumption, but not by
- It might allow us to use
Typeclasses Opaquefor all std++ operational type classes. As described in !914 (comment 91480), this is currently impossible.
We could probably do some bikeshedding about the name or other implementation aspects. But I might make sense to first check out the performance impact and whether it breaks anything in the reverse dependencies. So @jung could you run timing CI, please.