The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Jonathan --

A usual way to prevent this is to introduce a hypothesis at the end of the tactic and then look for it at the beginning and fail if you find it. It isn't the most elegant solution, but it does work. To be concrete (code untested):

Definition Stop := True.

Ltac my_tac :=

  match goal with | H : Stop |- _ => fail 1 | |- _ => idtac end ;

  ...your tactic... ;

  assert (Stop) by (exact I).

On Thu, May 1, 2014 at 3:15 PM, Jonathan <jonikelee AT gmail.com> wrote:

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

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/