coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automatic Indentation

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: Pierre Courtieu <pierre.courtieu AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Automatic Indentation
Date: Mon, 23 Jun 2014 10:32:57 -0400

> (add-hook
> 'proof-mode-hook
> '(lambda ()

Please don't quote your lambdas. That turns variables into symbols, and
we Coq users should know that variable bindings are much more subtle
beasts than "immutable strings ;-)

Stefan

[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