The Coq mailing list

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

On 10/06/2014 16:16, Pierre-Marie Pédrot wrote:
> No idea what fixed it though.

OK, I found the culprit. This is a totally undocumented, unused and
broken feature of Coq that was doing quadratic exploration of the stack
of definitions. By removing 10 lines of code, this solves the problem.
This patch should be considered for a pl, if people wish so.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature