The Coq mailing list

[Vladimir Komendantsky <Vladimir.Komendantsky AT sophia.inria.fr>]

Is this possible to write a tactic in the Ltac language that would match 
goals of the kind

|- (f ...) <= (g ...)

where arities of f and g are arbitrary? Also I have the same question 
regarding goals like

|- (match x with ...) <= (match y with ...)

where the bodies of match clauses are not cared about. I'm writing my 
tactic in OCaml but I'd be grateful if someone suggests me how to use 
Ltac for this purpose.

Vladimir