The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 05/16/2014 10:02 PM, Jason Gross wrote:
> You can also do [Hint Rewrite @my_rw_rule : rw_rules.], but this won't
> solve the constraints in the goal, it'll just leave them unsolved as
> further goals.
>
> -Jason

Thanks.  That form works in my case as well.

So, is the "Unable to satisfy" error a bug?  Probably not.  But I still 
don't understand the reason for the difference in behavior between Hint 
Resolve and Hint Rewrite with respect to implicit arguments.  Is Hint 
Rewrite foo ever preferable to Hint Rewrite @foo?

-- Jonathan