coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq runtime quadratic in number of definitions

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq runtime quadratic in number of definitions
Date: Tue, 10 Jun 2014 14:06:41 +0200

On 10/06/2014 14:05, Vladimir Voevodsky wrote:
> What is "backtracking mechanism"?

The ability to call 'Undo', or to go back in the IDE.

BTW, is this slowdown still here in trunk?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Coq runtime quadratic in number of definitions, James Lingard, 06/09/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Thomas Braibant, 06/10/2014
  - Re: [Coq-Club] Coq runtime quadratic in number of definitions, Vladimir Voevodsky, 06/10/2014
    - Re: [Coq-Club] Coq runtime quadratic in number of definitions, Pierre-Marie Pédrot, 06/10/2014
      - Re: [Coq-Club] Coq runtime quadratic in number of definitions, James Lingard, 06/10/2014
        
        Re: [Coq-Club] Coq runtime quadratic in number of definitions, Pierre-Marie Pédrot, 06/10/2014
        
        Re: [Coq-Club] Coq runtime quadratic in number of definitions, Pierre-Marie Pédrot, 06/10/2014
      - Re: [Coq-Club] Coq runtime quadratic in number of definitions, Vladimir Voevodsky, 06/10/2014