Right now, we use 'simultaneous' sequencing which has nice equational properties (it is the kleisli extension to the tactic monad). But in practice, I've found that we actually want to use the old 'sequential' one that I had hacked up originally. This one runs a tactic on a goal, performs a substitutions, runs the next thing, etc. The one we do now runs them all simultaneously, and then squishes everything.
Right now, we use 'simultaneous' sequencing which has nice equational properties (it is the kleisli extension to the tactic monad). But in practice, I've found that we actually want to use the old 'sequential' one that I had hacked up originally. This one runs a tactic on a goal, performs a substitutions, runs the next thing, etc. The one we do now runs them all simultaneously, and then squishes everything.
It's kind of funny...