Merge upstream changes #8
Merged
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
- Adds missing commas, including in if statement header. Other option is "these are actually if expressions". - Adds code formatting to "if" when referring to the keyword. Some instances do, some don't. Changed for consistency. - Fixes use of "e.g." and "i.e." (British English standards, rather than American English, which would use "e.g., __" or "i.e., __") - Replaces exposed HTML dfn tag with boldface mirroring introduction of "syntactic sugar" above.
- "becomes" -> "become" - Adds missing colons and commas - Removes dubious in "aesthetic value is doubtful dubious". Gotta pick one, and the sentence refers back to doubtful anyway. - "Recommanded" -> "Recommended" - "loosing" -> "losing" - Added needed "of" - "correspondent" -> "counterpart". I believe "corresponding function" was meant, this way avoids repeating "function". - "looking" -> "look" - "consider" -> "feels". Also updates matching clause below to enhance parallelism. - "nocive" -> "novice" (best guess) - "overuse or under-use them" reworded for clarity
Hugo Herbelin ( @herbelin ) reports that he mistakenly tried 4.02.0 and observed massive Coq compilation times. I'm trying to update the web-facing information to avoid users getting caught like this.
Fix typos/formatting
Fix typos in Guidelines
Update the link to the Camlp5 manual
Discourage use of 4.02.0
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.
No description provided.