Fixing capital letters in the "in" syntax of instantiate. #8110
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
This trace of V7 syntax remained unnoticed (since July 2004).
ppedrot
reviewed
Jul 23, 2018
|
After pondering a bit, I think this PR should probably deserve comments by more devs. I understand that it brings uniformity to a rarely used syntax, but let's summon people just in case by marking this PR a needing discussion. |
maximedenes
approved these changes
Aug 16, 2018
Anyone willing to discuss this PR after the summer breaks?
It does not. Definition Value := 0. (* ok *)The reason (to double-check) is that |
JasonGross
approved these changes
Sep 1, 2018
ppedrot
approved these changes
Sep 3, 2018
ppedrot
added a commit
that referenced
this pull request
Sep 6, 2018
proux01
added a commit
to proux01/bigenough
that referenced
this pull request
Dec 6, 2021
This was deprecated in coq more than three years ago in coq/coq#8110 and removed recently coq/coq#15193 (so will disappear in 8.16).
proux01
added a commit
to proux01/multinomials
that referenced
this pull request
Dec 14, 2021
This was deprecated in coq more than three years ago in coq/coq#8110 and removed recently coq/coq#15193 (so will disappear in 8.16).
thery
pushed a commit
to thery/multinomials
that referenced
this pull request
Jan 3, 2023
This was deprecated in coq more than three years ago in coq/coq#8110 and removed recently coq/coq#15193 (so will disappear in 8.16).
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.
This trace of V7-style capital letters in an admittedly uncommon syntax remained unnoticed for 14 years.
Kind: bug fix
Found by @zeimer (see #8072).
The PR is purely about the syntax side (not about the technical issues with
instantiate, #5378, #5504, #5505, ...).