Janno (Mar 01 2022 at 15:36): Janno (Mar 01 2022 at 15:36):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.
Paolo Giarrusso (Mar 01 2022 at 18:44):Are we missing some TC mode?
Matthieu Sozeau (Mar 25 2022 at 13:13):Or you have a wrong TC mode somewhere on which you want to backtrack
Last updated: Apr 18 2024 at 10:02 UTC