Hello,
I have a tactic, lets call it branch which creates, some number of goals. I have another tactic, let’s call it solve that solves the goal if there is enough information in the context. I want to apply combination of tactics in a depth-first manner. In other words, I want to branch, then try solve new goals, then branch in first goal only. Do this recursively until that branch of goal tree is solved, then jump into the next first goal. How can I achieve this?