slightly change notations to prevent conflict with : of ssreflect #112
Conversation
This file contains hidden or 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
|
All checked failed due to timeout (again). |
|
Hmm. I'm going to try reorganizing the Travis script. |
|
Could you merge master into your branch and then try again? |
|
I am very unhappy with this change. Why should an "only printing" notation cause a conflict with some other package? And why should ssreflect pollute my system and cause me to use an unnatural notation? Thank you, ildyria, for identifying the problem and proposing this fix, but I would really like to discuss this with the Coq team. Can you write a sentence or two that explains the situation? |
ildyria
force-pushed
the
ssReflect_notation_conflict
branch
from
2f57b88 to
a02fe41
Compare
ildyria
force-pushed
the
ssReflect_notation_conflict
branch
from
c8fdf99 to
f191c3d
Compare
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.
Proposed to solve: #111
rename
:by<:.