The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is there a variant of [etransitivity] that accepts an argument, so that I can help Coq along in figuring out how to do transitivity?  That is, is there a tactic that I can pass along an _expression_ [expr], which has some underscores in it, and which will do something like

    match goal with

      | [ |- @eq ?A ?a ?b ] => eapply (@eq_trans A a foo b)

    end.

except that it will work with any parametric relation declared to be transitive?

If I try [etransitivity foo], I get

Toplevel input, characters 35-36:

Syntax error: '.' or '...' expected after [tactic:tactic] (in [proof_mode:subgoal_command]).

Thanks!

-Jason