The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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