Hello,
Inductive and Variant are not indented the same, as demonstrated by the following example:
Inductive three: Type :=
| One
| Two
| Three
.
Variant three': Type :=
| One'
| Two'
| Three'
.
I believe the expected behaviour is thatVariant should be indented like Inductive.
I'm on PG's last commit with Emacs 30.2.
Thanks!
Hello,
InductiveandVariantare not indented the same, as demonstrated by the following example:I believe the expected behaviour is that
Variantshould be indented likeInductive.I'm on PG's last commit with Emacs 30.2.
Thanks!