The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

  As suggested by Cedric it might fail because just the first occurrence can be rewritten,

otherwise it’s probably a bug indeed. Note that rewrite at has a different semantic (it’s counting

occurrences of the first complete unification appearing in the goal). The bug tracker is 

inaccessible right now…

— Matthieu

Le 10 mars 2014 à 09:34, Jason Gross <jasongross9 AT gmail.com> a écrit :

Hi,

Can someone explain to me the difference between [setoid_rewrite ... at 1] and [setoid_rewrite ...]?  In particular, why might the first succeed when the second fails?  (This seems to me to be a bug, so I reported it, with a test case, at https://coq.inria.fr/bugs/show_bug.cgi?id=3253.)

Thanks,

Jason