The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I find my self writing the pattern

  match goal with

    | [ _ : appcontext[foo] |- _ ] => bar foo

    | [ |- appcontext[foo] ] => bar foo

  end

(where [foo] is some _expression_, possibly with patterns and blanks that can't be inferred just from context, and bar is some tactic that gets applied to those pattern variables) a lot.  Often, [bar] takes the form of [change ... with ... in *] or [rewrite ... in *].  Is there a way of writing [match goal with ...] that combines these two, so I don't have to duplicate tactic code?

Thanks.

-Jason