The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Just to give a little more background on the test case, this Ltac attempts to implement a primitive backtracking.  The idea is to find two matching AbsVar leaf nodes one in each of the two trees passed in as parameters.  The case that freezes is one which should fail as neither of the trees passed in have an AbsVar leaf node.  Does auto implement backtracking?  My impression was that it just keeps applying its rules until none are applicable.

         - Ken

> From: thomas.braibant AT gmail.com
> Date: Fri, 29 Jul 2011 00:15:05 +0200
> Subject: Re: [Coq-Club] Ltac infinite loop (or at least very slow
> To: kendroe AT hotmail.com
>
> Why do not you use auto in this particular example ? auto with the
> lemmas you apply by hand....
>
> thomas
>
>
>
> On Fri, Jul 29, 2011 at 12:07 AM, Kenneth Roe <kendroe AT hotmail.com> wrote:
> > Thanks to everyone who responded to my previous email on existential
> > variables.  I've now solved that issue.
> >
> > Now on to the next issue--the call to the tactic solvePick2Vars at the very
> > end of the example I've attached seems to go into an infinite loop (or at
> > least is very slow).  Can anyone tell me what is happening?
> >
> >                - Ken
> >