coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reset Induction Principle

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Damien Pous <Damien.Pous AT ens-lyon.fr>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Reset Induction Principle
Date: Sat, 6 Mar 2010 21:41:16 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=NsWIN3bIP+cnrLA3DSC5AbGoF845FkFzkhpQduRyjEroEcwGPe0zmWHpaFN4DkS1fb Hon2TAprD4HBioayyIk6dQwOHiVDBBYdZsU/jIDy5mHHRD46do7EEclqtzMAqcrMrOv3 OFXC5tJM6pesTExKAUo6+SYeBZtDJxo5o+jKw=

Why not use comments to keep track failed attempts?

Pierre

2010/3/5 Damien Pous
<Damien.Pous AT ens-lyon.fr>:
> 2010/3/4 Pierre Courtieu
> <Pierre.Courtieu AT cnam.fr>:
>> No this is not a bug. These commands are supposed to be used when
>> using coq in a terminal. Using these command in coqide would
>> de-synchronize the "locked region" of the buffer and coq typing
>> environment.
>
> What about "Abort", which does not raise such a problem (I think) ?
> (I find Abort quite useful, to keep track of failed attempts.)
>
> Damien
>

Re: [Coq-Club] Reset Induction Principle, catalin . hritcu
- Re: [Coq-Club] Reset Induction Principle, Pierre Courtieu
  - Re: [Coq-Club] Reset Induction Principle, Catalin Hritcu
  - Re: [Coq-Club] Reset Induction Principle, Damien Pous
    - Re: [Coq-Club] Reset Induction Principle, Pierre Courtieu
      - Re: [Coq-Club] Reset Induction Principle, Adam Chlipala
        
        Re: [Coq-Club] Reset Induction Principle, Pierre Courtieu