coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reset Induction Principle

From: Damien Pous <Damien.Pous AT ens-lyon.fr>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Reset Induction Principle
Date: Fri, 5 Mar 2010 09:27:15 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type; b=GGZjLXoVPK/vANhwRtA2d7lj2PxtxlbJDg3PydHN0iZd8/ebH43R5ghbOb6jUh9hwb Wt1wnj390KazjPnqry33b/14ZHeUabpoOpy2KmtFJyC5JIetxz51dSuQoyignkOBedQK mk+08HsrgkXUrB35DwzKcq/Ro3ZVVosMRQAYo=

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