Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #948: [doc] Write (@nil nat) instead of (nil nat) | Maxime Dénès | 2017-08-16 |
|\ | |||
* \ | Merge PR #943: Reference Manual: minor wording improvements | Maxime Dénès | 2017-08-16 |
|\ \ | |||
* \ \ | Merge PR #940: Replace jarring use of "Remark" with "Note" | Maxime Dénès | 2017-08-16 |
|\ \ \ | |||
* \ \ \ | Merge PR #934: Fix some coq-tex errors in the reference manual. | Maxime Dénès | 2017-08-16 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | 2017-08-16 |
|\ \ \ \ \ | |||
| | | | | * | Update Setoid.tex | larsr | 2017-08-02 |
| |_|_|_|/ |/| | | | | | | | | | The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`. | ||
| * | | | | Typo in the documentation of cumulativity | Amin Timany | 2017-08-02 |
| | | | | | |||
| | | * | | Improve style slightly | Sam Pablo Kuper | 2017-08-01 |
| | | | | | | | | | | | | | | | | | | | | | | | | | per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940). | ||
* | | | | | Merge PR #933: Fix documentation of Hint Mode (bug #4911). | Maxime Dénès | 2017-08-01 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #932: Fix shuffled documentation. | Maxime Dénès | 2017-08-01 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #929: Add missing paragraph to introduction | Maxime Dénès | 2017-08-01 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #925: Document Extraction TestCompile | Maxime Dénès | 2017-08-01 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | Maxime Dénès | 2017-08-01 |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | Fix incorrect use of "At the end". | Sam Pablo Kuper | 2017-07-31 |
| | | | | | | | | | | |||
| | | | | | | | | * | Minor grammar fix: replace a "then" with a "so". | Sam Pablo Kuper | 2017-07-31 |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
| | | | | | | | * | Replace jarring use of "Remark" with "Note" | Sam Pablo Kuper | 2017-07-31 |
| |_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | or with nothing at all, to improve readability for native English speakers. Editors may wish to remove such constructions altogether in future revisions, per general style guidance such as: - https://en.wikipedia.org/wiki/Wikipedia:%22Note_that%22_is_unnecessary - https://english.stackexchange.com/a/238142/7318 - http://blog.apastyle.org/apastyle/2015/09/principles-of-writing-how-to-avoid-wordiness.html | ||
| | | | | | * | | Update documentation of cumulativity | Amin Timany | 2017-07-31 |
| | | | | | | | | |||
| | | | | | * | | Fix typo and Add Jason's example to the doc | Amin Timany | 2017-07-31 |
| | | | | | | | | |||
| | | | | | * | | Improve documentation of cumulativity | Amin Timany | 2017-07-31 |
| |_|_|_|_|/ / |/| | | | | | | |||
| | | * | | | | Drop paragraph mentioning Addendum as separate doc. | Théo Zimmermann | 2017-07-29 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | As suggested by @herbelin. | ||
* | | | | | | | Merge PR #823: Async off in Windows by default in CoqIDE | Maxime Dénès | 2017-07-28 |
|\ \ \ \ \ \ \ | |||
| | | | | | | * | Fix some coq-tex errors in the reference manual. | Guillaume Melquiond | 2017-07-28 |
| |_|_|_|_|_|/ |/| | | | | | | |||
| | | | | | * | Fix documentation of Hint Mode (bug #4911). | Guillaume Melquiond | 2017-07-28 |
| |_|_|_|_|/ |/| | | | | | |||
| | | | | * | Fix shuffled documentation. | Guillaume Melquiond | 2017-07-28 |
| |_|_|_|/ |/| | | | | |||
| | | | * | Add missing paragraph to introduction | Benjamin Pierce | 2017-07-27 |
| |_|_|/ |/| | | | |||
| | | * | Extraction.tex: mention the possible "From Coq Require Extraction" | letouzey | 2017-07-27 |
| | | | | |||
| | | * | Extraction TestCompile documented + mentionned in CHANGES | Pierre Letouzey | 2017-07-27 |
| |_|/ |/| | | | | | | | | Also includes a minor fix of the Extraction doc (a Require was missing). | ||
| | * | [toplevel] Remove long ago deprecated and NOOP options. | Emilio Jesus Gallego Arias | 2017-07-27 |
| |/ |/| | | | | | Minor clean up, no sense in having these as they do nothing. | ||
* | | Adding a V8.7 compatibility version number. | Hugo Herbelin | 2017-07-21 |
| | | |||
* | | Merge branch 'v8.7' | Maxime Dénès | 2017-07-20 |
|\ \ | |||
| * \ | Merge PR #745: Add timing scripts | Maxime Dénès | 2017-07-19 |
| |\ \ | |||
* | \ \ | Merge PR #865: RefMan-ext: fix some typos | Maxime Dénès | 2017-07-17 |
|\ \ \ \ | |||
| * | | | | Update with non structurally recursive | william-lawvere | 2017-07-14 |
| | | | | | |||
| | * | | | Sync the manual with the deprecation warnings. | Théo Zimmermann | 2017-07-11 |
| |/ / / |/| | | | |||
| | * | | Document the timing targets | Jason Gross | 2017-07-11 |
| | | | | | | | | | | | | | | | | | | | | We document the most useful timing targets and variables, how to invoke them, and what the output looks like. | ||
| | * | | Strip trailing spaces | Jason Gross | 2017-07-11 |
| |/ / |/| | | |||
| * | | RefMan-ext: fix some typos | William Lawvere | 2017-07-07 |
| | | | |||
* | | | Merge PR #842: Update the Tutorial. | Maxime Dénès | 2017-07-07 |
|\ \ \ | |||
* \ \ \ | Merge PR #835: Remove doc/refman/RefMan-ind.tex | Maxime Dénès | 2017-07-07 |
|\ \ \ \ | |_|/ / |/| | | | |||
* | | | | Merge PR #837: Add inversion_sigma to CHANGES and to doc | Maxime Dénès | 2017-07-05 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn | Maxime Dénès | 2017-07-05 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #832: Document an example `Makefile` for `coq_makefile` | Maxime Dénès | 2017-07-05 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-07-04 |
|\ \ \ \ \ \ \ | |||
| | | * | | | | | Update RefMan-syn.tex | william-lawvere | 2017-07-01 |
| | | | | | | | | |||
| | | * | | | | | Merge remote-tracking branch 'upstream/trunk' into trunk | William Lawvere | 2017-07-01 |
| | | |\ \ \ \ \ | |_|_|/ / / / / |/| | | | | | | | |||
| | | * | | | | | RefMan-gal: improve grammar | William Lawvere | 2017-07-01 |
| | | | | | | | | |||
| | | * | | | | | RefMan-syn: grammar edit | William Lawvere | 2017-07-01 |
| | | | | | | | | |||
| | * | | | | | | Document an example `Makefile` for `coq_makefile` | Jason Gross | 2017-06-30 |
| |/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | We document an example `Makefile` which does not include the generated `CoqMakefile`, but instead invokes arbitrary targets in it. | ||
| | | | * | | | Remove doc/refman/RefMan-ind.tex | Jason Gross | 2017-06-30 |
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | It does not seem to be referred to by any file, and does not seem to be built by any implicit rules. | ||
| | | * | | | Add doc for inversion_sigma to RefMan-tac | Jason Gross | 2017-06-30 |
| |_|/ / / |/| | | | |