coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] PG indentation

From: Beta Ziliani <bziliani AT famaf.unc.edu.ar>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] PG indentation
Date: Mon, 12 Sep 2016 17:26:40 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bziliani AT famaf.unc.edu.ar; spf=None smtp.mailfrom=bziliani AT famaf.unc.edu.ar; spf=None smtp.helo=postmaster AT famaf.unc.edu.ar
Ironport-phdr: 9a23:jmknbx97TOOi/P9uRHKM819IXTAuvvDOBiVQ1KB90uocTK2v8tzYMVDF4r011RmSDNydtaIP0raJ++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Dq3PF4XTl8W60fyps92WOl0QxWn1XbQnBxKv5S7Vq8Ne1YBlM+M6zgbDinpOYeVfg21ycwG9hRH5s+294JcrwSVUuvsn9oYUW7f7e6UxS71wAj0jOm5z+cvg8xTPUE2G/C1PAS0tjhNUDl2dv1nBVZDrv36/77Il1Q==

Stefen and Clement, you nailed it entirely. It's the
electric-indent-mode what is doing all this.

On Mon, Sep 12, 2016 at 5:07 PM, Clément Pit--Claudel
<clement.pit AT gmail.com>
wrote:
>
> Otherwise, adding a parens fixes it: (x <- …). In general, I don't think
> you can expect PG to indent your notations properly, at least not without
> support from Coq.

Of course, I wasn't expecting it. And it makes perfect sense when you
think of tacticals.
It'd be very helpful to have some help from Coq notations to do the indent!

[Coq-Club] PG indentation, Beta Ziliani, 09/12/2016
- Re: [Coq-Club] PG indentation, Clément Pit--Claudel, 09/12/2016
  - Re: [Coq-Club] PG indentation, Beta Ziliani, 09/12/2016
    - Re: [Coq-Club] PG indentation, Clément Pit--Claudel, 09/12/2016
      - Re: [Coq-Club] PG indentation, Beta Ziliani, 09/12/2016
    - Re: [Coq-Club] PG indentation, Stefan Monnier, 09/12/2016