coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automatic Indentation

From: "Strub, Pierre-Yves" <pierre-yves AT strub.nu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Automatic Indentation
Date: Fri, 20 Jun 2014 17:46:15 +0200

On 2014-06-20 17:10, Pierre Courtieu wrote:

Beware that you need to follow the precedence - > +> * to make
indentation work. Nesting bullets inside { } is supported.

Hi,

Which is a total nightmare for people doing ssreflect by the way and having scripts not following this precedence.

Indenting with spaces is soooo cool...

Best,
-- Pierre-Yves.

[Coq-Club] Automatic Indentation, Julien Narboux, 06/17/2014
- Re: [Coq-Club] Automatic Indentation, Bas Spitters, 06/18/2014
  - Re: [Coq-Club] Automatic Indentation, Eelis van der Weegen, 06/18/2014
    - Re: [Coq-Club] Automatic Indentation, Julien Narboux, 06/19/2014
      - Re: [Coq-Club] Automatic Indentation, Pierre Courtieu, 06/20/2014
        
        Re: [Coq-Club] Automatic Indentation, Julien Narboux, 06/20/2014
        
        Re: [Coq-Club] Automatic Indentation, Pierre Courtieu, 06/20/2014
        
        Re: [Coq-Club] Automatic Indentation, Strub, Pierre-Yves, 06/20/2014
        Re: [Coq-Club] Automatic Indentation, Pierre Courtieu, 06/23/2014
        Re: [Coq-Club] Automatic Indentation, Stefan Monnier, 06/23/2014
        
        Re: [Coq-Club] Automatic Indentation, Jonathan, 06/20/2014
        Re: [Coq-Club] Automatic Indentation, Pierre Courtieu, 06/23/2014