The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

Dear Clément,

Thanks for looking into this.

The settings:

Coq Indent Box Style: off (nil)
Coq Script Indent: off (nil)

Here is some test code:

Example indent_test : True.
Proof.
  let why_this_is_indentend :=
      and why this is here in
  x <- some MetaCoq code;
    y <- ouch this shouldnt be indented;
    ret why_isnt_this_indented_BTW.
Qed.

I prefer to set the tab as two spaces, and mange it myself. But Proof
General is inserting its own indentation (and sometimes in a weird
way, see e.g. the two lines ending with ;).

And what is really pissing me off is that it is changing the
indentation I wrote. For instance, if I decide to move the y <- ouch
... code so it is aligned with the previous line, after hitting enter
PG will move it back to where it is in the code above. Maybe there are
some other options I’m missing?

Best,
Beta

On Mon, Sep 12, 2016 at 3:58 PM, Clément Pit--Claudel
<clement.pit AT gmail.com>
 wrote:
> Hi Beta,
>
> How do you set these settings? Can you share a snippet and show the 
> expected indentation?
>
> Cheers,
> Clément.
>
> On 2016-09-12 14:47, Beta Ziliani wrote:
>> Hi list,
>>
>> I updated PG and now it is indenting my code in a way I don't want it
>> to. I'm aware of the options Coq Script Indent and Coq Indent Box
>> Style, however they seem to have no effect whatsoever. Any clues?
>>
>> Thanks,
>> Beta
>>
>