I have a habit of leaving holes and letting PG tell me the type needed to fill each one by one, but I'm dealing with a typeclass heavy domain right now and most of the holes lead to very long/indefinite spinning looking for an instance and then an error on the whole term, not the "next" hole. Is there a way to tell coq not to try using typeclass resolution for some hole?
Also, sometimes using Hint Modes can help: It allow to tell Coq that typeclasses should only be searched if a subset of Parameteres is evar-free by treating them as "input". https://coq.inria.fr/refman/proof-engine/tactics.html#coq:cmdv.hint-mode
If you're creating a typeclass you should certainly consider if it needs a Hint Mode.
Sometimes, ditto if your libraries create them but have arguably bugs.
Last updated: Feb 01 2023 at 11:04 UTC