coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ltac infinite loop (or at least very slow

From: Kenneth Roe <kendroe AT hotmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Ltac infinite loop (or at least very slow
Date: Thu, 28 Jul 2011 15:07:47 -0700
Importance: Normal

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

Attachment: test.v
Description: Binary data

[Coq-Club] Ltac infinite loop (or at least very slow, Kenneth Roe
- Message not available
  - RE: [Coq-Club] Ltac infinite loop (or at least very slow, Kenneth Roe
- Re: [Coq-Club] Ltac infinite loop (or at least very slow, Adam Chlipala
  - RE: [Coq-Club] Ltac infinite loop (or at least very slow, Kenneth Roe