Custom Query (361 matches)

PG indents as follows

Goal True.
constructor.
Qed.

Goal True.
Proof.
  constructor.
Qed.

And similarly for Proposition, Fixpoint, Instance, Corollary, and possibly some others. (Definition, Theorem, Lemma, and Let all work fine)

Here is some code indented by TAB:

Goal True.                                                                                                                                  
Proof.
  match goal with
    | _ => exists 1
                | _ => idtac
                  end.

Here's some code formatted by TAB in emacs PG:

Definition A
: { T : ReallySuperDuperExtremelyLongName bar baz qux &
                                          foo T }.
  Definition B
  : { T : (ReallySuperDuperExtremelyLongName bar baz qux) &
                                                          foo T }

      Definition C
  : { T : ReallySuperDuperExtremelyLongName bar baz qux
                                            & foo T }.
    Definition D
    : { T : (ReallySuperDuperExtremelyLongName bar baz qux)
              & foo T }

The indentation of Definition is clearly broken. Additionally, I think all of them should be formatted roughly like Definition D, where the & or the foo is lined up close to the start of the line, rather than as an argument of ReallySuperDuperExtremelyLongName. I'd be even happier if sigT notation were formatted like sig notation, that is, if & acted like | here. (This change doessn't fix the screwy levels of Definition, though.)