The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

I asked a similar question, a few months ago. After some
investigation, it turned out that the most likely culprit was the
backtracking mechanism.

HTH

On Mon, Jun 9, 2014 at 1:58 PM, James Lingard 
<jchl2 AT cam.ac.uk>
 wrote:
> The runtime of coqc on the following program:
>
>   Definition n0 := 0.
>   Definition n1 := 0.
>   Definition n2 := 0.
>   ...
>   Definition nN := 0.
>
> appears to be roughly quadratic in the number of definitions.
>
> Does anyone know what causes this?
>
> Thanks,
> James.
>