Is there any way to say "by default, for any implicit argument of this type, use this tactic to try to fill it in"?
You could make that type a typeclass, and provide an Hint Extern for it.
But it's not a safe refactoring, and you also get any other instance: those declared as such, and any local assumptions.
(still probably what I'd try)
If you change the requirements quite a bit more, tactics-in-terms (ltac:(...)) might be relevant, if you haven't seen those
Yeah, this was my backup
Last updated: Jan 29 2023 at 05:03 UTC