Stream: Coq devs & plugin devs

Topic: TC search best_effort returning invalid results


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 18:44):

Are we missing some TC mode?

view this post on Zulip Matthieu Sozeau (Mar 25 2022 at 13:13):

Or you have a wrong TC mode somewhere on which you want to backtrack


Last updated: Oct 13 2024 at 01:02 UTC