Indentation is wrong after [exists]

[proofgeneral]

Indentation is wrong after [exists]

[cpitclaudel]

I think that's a known issue with any Goal form following a quantifier actually:

Goal forall t: bool, t = t.
                       reflexivity.
Qed.

[Matafou]

Yes it is known and a bit hard to fix in general.

Workaround: put Proof at start of a proof.

The reason it is hard to fix is that it needs to detect if a command is a
proof start or not. It is not trivial.

P

Le mercredi 13 janvier 2016, Clément Pit--Claudel [email protected]
a écrit :

I think that's a known issue with any Goal form following a quantifier
actually:

Goal forall t: bool, t = t.
reflexivity.
Qed.

—
Reply to this email directly or view it on GitHub
#29 (comment).

[Matafou]

But I will try to have something less wrong anyway.

FYI if you don't like indentation induced by "Proof" you can set

(setq coq-indent-proofstart 0)

P.

2016-01-13 22:36 GMT+01:00 Pierre Courtieu [email protected]:

Yes it is known and a bit hard to fix in general.

Workaround: put Proof at start of a proof.

The reason it is hard to fix is that it needs to detect if a command is a
proof start or not. It is not trivial.

P

Le mercredi 13 janvier 2016, Clément Pit--Claudel <
[email protected]> a écrit :

I think that's a known issue with any Goal form following a quantifier
actually:

Goal forall t: bool, t = t.
reflexivity.
Qed.

—
Reply to this email directly or view it on GitHub
#29 (comment).

[Matafou]

Should be fixed.
Notice that in some ugly cases the "goal starting" property of a command will not be detected and indentation may be broken. Use "Proof" to workaround.