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: Feb 06 2023 at 20:02 UTC