Currently, ntac cannot skip a subgoal to solve another one first. This makes it difficult to compose tactics and automate proofs, e.g., with try.
Still thinking about the right code organization, but I think part of the problem is that most tactics call fill themselves (which calls next), which makes the traversal order fixed. Ideally, fill and next would be pulled out of the tactics themselves (into the main loop?), but other tactic(al)s could then specify a different traversal (like coq ;).
Currently, ntac cannot skip a subgoal to solve another one first. This makes it difficult to compose tactics and automate proofs, e.g., with
try.Still thinking about the right code organization, but I think part of the problem is that most tactics call
fillthemselves (which callsnext), which makes the traversal order fixed. Ideally,fillandnextwould be pulled out of the tactics themselves (into the main loop?), but other tactic(al)s could then specify a different traversal (like coq;).