Stream: Coq devs & plugin devs

Topic: testing delayed constraints

Gaëtan Gilbert (Apr 04 2023 at 12:25):

Anyone know a reliable way to get an unsolvable delayed constraint from a tactic?
so eg tac; gfail. would say "tactic failure" but tac. would error in the implicit constraint solving

Last updated: Nov 29 2023 at 22:01 UTC