The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

But the tactic

  progress repeat

  match goal with

  | [H1 : _ |- _] => progress (

    apply (proj1 OJQZ) in H1 ||

    (apply eq_sym in H1; apply (proj1 OJQZ) in H1; try apply eq_sym in H1))

  | [|- _] => progress (

    apply (proj2 OJQZ) ||

    (apply eq_sym; apply (proj2 OJQZ); try apply eq_sym))

  end.

is just the result of "unfolding" rw_aux OJQZ. Why does that one work, but not the other?

I've made the argument of OJQZ implicit just so I could feed it to proj1 and proj2.