coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: Matthieu Sozeau <mattam AT mattam.org>
Cc: Thomas Braibant <thomas.braibant AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Dreadful performance of setoid rewrite in Coq 8.3-beta & trunk.
Date: Fri, 11 Jun 2010 11:00:48 +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; b=rnFFwbfww4WejJx4A4drL69x3CRoeEVyuQlntLpRfu317LUmp5mihwhwVs1xlml6ry AfWZ0epEd7mV1ulaaRtZrmiGxBQG4le+Ed4GYzUOrKP6/+2vL0h74jJ1JAjpAt0B5kNi Q8YF1SwBj2VMgZJswwdkJN4Nn3ebX6APrNdZo=

��Dear�Matthieu,

Then all examples go through in reasonable time. I will add these to the standard library and fix the dangerous instances as well.

��Indeed, that helps. Thanks a lot for your help!

��Btw. is there any reasonable way to "debug" resolution to figure out what's going on, in cases such as this one?

��Best,

��Adam

--
Adam Koprowski � [http://adam-koprowski.net]
R&D @ MLstate � �[http://mlstate.com, 15 rue Berlier, 75013 Paris, France]

[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