coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: Adam Koprowski <adam.koprowski AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk.
Date: Thu, 10 Jun 2010 15:25:53 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=VbJWAuY5HsrjxQkI04WBZOTLVBN9/hLiRBZ0iVT4QgjB5pw3kPZQGbyXjSkNmtQhqY nlGpYhFoGgmZwwId1BD5SKqV4QYTc0amjiDeEEGXW+V6gjfxm5vGhGep8y4b5SefAiam i+LUfyb8SXYeYek1PAbNXfFF26DyIBS8yjKkg=

>
> ��I'm not sure I understand, why cannot you just [Print] the lemma?
> �� Adam

Just because it took 1500 seconds on my laptop computer.

[Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Adam Koprowski
- Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., AUGER Cedric
- Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Thomas Braibant
  - Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Adam Koprowski
    - Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Thomas Braibant
  - Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Matthieu Sozeau
    - Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., Adam Koprowski
      - Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk., St�phane Lescuyer