The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/01/2013 08:09 PM, Rui Baptista wrote:
> 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.

When I run your tactic that fails, I literally see an error message 
saying that the parameter of [OJQZ] can't be inferred, so that seems 
pretty clearly to be the problem.  The extra context of [apply] is 
sufficient to determine the parameter, perhaps because of some magic in 
the [apply] implementation that can only be achieved in OCaml, not in 
your own Ltac definitions.