Is there a way to disable the best_effort
strategy during typechecking? The upgrade to 8.15 broke at least one of our proofs because instead of keeping a bunch of evars for typeclasses unresolved, Coq now makes partial progress on some of them in a way that makes the resulting goal unprovable.
Are we missing some TC mode?
Or you have a wrong TC mode somewhere on which you want to backtrack
Last updated: Oct 13 2024 at 01:02 UTC