The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

What is "backtracking mechanism"?
V.

On Jun 10, 2014, at 10:58 AM, Thomas Braibant 
<thomas.braibant AT gmail.com>
 wrote:

> 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.
>>