The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I'm trying to write an extern hint for eauto that does some 
rearrangement of terms for the benefit of other eauto hints. 
Unfortunately, this hint sometimes causes eauto to loop forever because 
it is always applicable immediately after itself (and there isn't any 
easy way to make it fail only after itself).

 It seems I could break the loop if I could force eauto to take any 
lower cost step prior to using that hint again.

Does anyone know if there is a way to accomplish this?

-- Jonathan