The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Dear Adam

I'm not sure I understood your problem exactly, but maybe one of the
things here might help you:
http://coq.inria.fr/refman/Reference-Manual028.html#toc143

Cheers

2010/9/20 Adam Megacz 
<megacz AT cs.berkeley.edu>:
>
> The "<num>:<tactic>" syntax makes it possible to apply a tactic to a
> specific subgoal; for example:
>
>  3:simpl.
>
> Is there a version of this which applies a tactic to all subgoals?  I
> tried the obvious
>
>  *:simpl.
>
> But that's not valid syntax.
>
> The case where this matters most (to me, at least) is when an [Instance]
> declaration using the { ; ; } syntax generates a large number of
> subgoals which can all be discharged with the same tactic; for example
>
>  Instance foo : bar :=
>  { baz := blah
>  }.
>  (* many obligations remain here *)
>
> In the past I've rewritten this sort of thing as
>
>  Instance foo : bar.
>    apply Build_bar with (baz:=blah)
>    ; magical_tactic.
>    Defined.
>
> But that's probably not the ideal way to go about this and is a bit less
> pleasant for people reading the proof.
>
> I suppose I could also use [Program Instance] and [Solve All Obligations
> using]; I'm just wondering if there's another solution.
>
> Thanks,
>
>  - a
>
>