The Coq mailing list

["Gransden, Thomas" <tg75 AT student.le.ac.uk>]

Hi all,

I was just wondering if there was a way of encoding the following scenario in Ltac:

Say that we have a few sequences of tactics that we use often in a corpus of proofs - for example lets say the following:

t1 - intros. rewrite mult_n_O. trivial.

t2 - intros. destruct_all bool. reflexivity.

t3 - induction n. intros. simpl; trivial. simpl; trivial.

Can I create an Ltac tactic that applies t1 OR t2 OR t3?

I have had a play around with Ltac but cannot seem to get something like this working, so any help or hints would be much appreciated.

Thanks

Tom