Warning about too many tactics in [_, _, ..., _]

[favonia]

The trailing tactics in [t1, t2, t3, ..., tn] will not run if the number of subgoals is less then the number of tactics, and that should generate a warning.

[jonsterling]

@favonia I'm not sure if it really should generate a warning, because the shape of the proof state is dynamic. But I'm not strongly against it either...

[favonia]

I think it is confusing if part of the script is silently ignored. The warning will be generated dynamically. Maybe I misunderstood your concern? Are you worried about the tactic defined in the userland?

[jonsterling]

@favonia I guess I was thinking that one doesn't want a script to depend that sharply on the actual structure of the proof state, but now I think you're right and I was wrong.

With that said, what I think we do want to allow is to provide fewer tactics than needed; for instance [t1,t2] should be fine, even if there are four subgoals. But we can make a warning if there are too many tactics provided.

[favonia]

Yes: being lazy is fine, but working too hard is a serious problem.