Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Vladimir Voevodsky <vladimir AT ias.edu>
  • To: coq-club AT inria.fr, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • Cc: "Prof. Vladimir Voevodsky" <vladimir AT ias.edu>
  • Subject: Re: [Coq-Club] Coq runtime quadratic in number of definitions
  • Date: Tue, 10 Jun 2014 14:28:49 +0200

On Jun 10, 2014, at 2:06 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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.


But the original message mentions coqc not coqtop.

V.



Archive powered by MHonArc 2.6.18.

Top of Page