Indent body and type when printing local definitions over several lines #18928
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
herbelin
added
kind: enhancement
coqbot-app
bot
added
the
needs: full CI
proux01
approved these changes
Apr 12, 2024
|
@herbelin apparently this requires modifying a few output tests |
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+indent-long-decls-printing
branch
from
6ef96ff
to
8cfba2a
Compare
coqbot-app
bot
removed
request: full CI
OK. I seized then the opportunity to also "improve" the printing of multiple names of same type. |
SkySkimmer
reviewed
Apr 12, 2024
proux01
reviewed
Apr 12, 2024
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+indent-long-decls-printing
branch
from
8cfba2a
to
2cb8e09
Compare
coqbot-app
bot
removed
the
request: full CI
proux01
reviewed
Apr 13, 2024
proux01
force-pushed
the
master+indent-long-decls-printing
branch
from
2cb8e09
to
c3e41f0
Compare
coqbot-app
bot
added
the
needs: full CI
For instance:
Theorem T (long_long_long_long_long_long_long_long_ident := fun x : nat => x) : True.
Before:
long_long_long_long_long_long_long_long_ident :=
fun x : nat => x : nat -> nat
============================
True
After:
long_long_long_long_long_long_long_long_ident :=
fun x : nat => x : nat -> nat
============================
True
At the same time, we:
- improve the printing of multiple variables with same time (see test-suite)
proux01
force-pushed
the
master+indent-long-decls-printing
branch
from
c3e41f0
to
55fc795
Compare
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
@proux01 are you going to self assign? Looks like the iris output tests are sensitive to this change, cc @RalfJung, @robbertkrebbers |
|
The Iris issue should be fixed now, sorry for the inconvenience. |
|
Thanks a lot |
|
@coqbot merge now |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Assume:
Theorem T (long_long_long_long_long_long_long_long_ident := fun x : nat => x) : True.Before the PR, it is printed
long_long_long_long_long_long_long_long_ident := fun x : nat => x : nat -> nat ============================ TrueAfter, it is printed:
long_long_long_long_long_long_long_long_ident := fun x : nat => x : nat -> nat ============================ TrueThe PR also applies this indentation to other similar places.
Overlays (to be merged before the current PR)