coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coq 8.5 is out!
- Date: Mon, 25 Jan 2016 15:05:14 +0100
On 25/01/2016 14:16, Jacques-Henri Jourdan wrote:
> Maybe this is due to the universe algorithm. Have you tried my patch
> (included in trunk but not in 8.5 currently) ?
Quick perfing suggests there may be a ~15% improvement with your patch,
but this would need testing to be confirmed.
@Frédéric: are there precise lines of code that got worse between 8.4
and 8.5 (let's say in rpo.v)? If so, could you give them so I can try to
guess what changed between the two?
PMP
Attachment:
signature.asc
Description: OpenPGP digital signature
- Re: [Coq-Club] Coq 8.5 is out!, (continued)
- Re: [Coq-Club] Coq 8.5 is out!, Enrico Tassi, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Enrico Tassi, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Jacques-Henri Jourdan, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Pierre-Marie Pédrot, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Emilio Jesús Gallego Arias, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Guillaume Melquiond, 01/25/2016
- Re: [Coq-Club] Coq 8.5 is out!, Frédéric Blanqui, 01/26/2016
- Re: [Coq-Club] Coq 8.5 is out!, Pierre-Marie Pédrot, 01/26/2016
- Re: [Coq-Club] Coq 8.5 is out!, Jacques-Henri Jourdan, 01/26/2016
- Re: [Coq-Club] Coq 8.5 is out!, Maxime Dénès, 01/26/2016
Archive powered by MHonArc 2.6.18.