The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi Marco,

This depends on the tactic that you want to try. If it takes an argument then you should be able to do something  like:

Ltac try_on_all tac :=

  repeat (match goal with 

            | [ H : _ |- _ ] => try (tactic H); generalize H; clear H

          end); intros.

Here, you're going to try the tactic on the hypothesis and then remove it from the hypothesis list using generalize and clear, at the end, you reintroduce all the hypotheses. The only problem with this script is that it will break all your hypothesis names.

Hope this helps.

On Tue, Jul 26, 2011 at 7:46 AM, Marco Servetto <marco.servetto AT gmail.com> wrote:

Hi, I'm wondering if there is a simple way to *try* a tactic over all
the hypothesis.
(of course is useful to put itself into a tactic)

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/