The Coq mailing list

[Eric Mullen <emullen AT cs.washington.edu>]

Is what you want similar to:

try solve [tactic1]; try solve [tactic2]....

On Oct 27, 2014 1:26 PM, "Gransden, Thomas" <tg75 AT student.le.ac.uk> wrote:

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