| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler | |
| 2017-08-17 | Merge PR #974: Change section caption, improve some wording | Maxime Dénès | |
| 2017-08-17 | Document anonymous universes (PR #544). | Gaëtan Gilbert | |
| 2017-08-16 | mention that tactic is the identity or gives error | Paul Steckler | |
| 2017-08-16 | change section caption, improve some wording | Paul Steckler | |
| 2017-08-16 | Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style | Maxime Dénès | |
| 2017-08-16 | 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-02 | Rewording the introduction | Enrico Tassi | |
| The contents should be exactly the same. I removed the distinction between tactical and pseudo-tactical because I think that it is too much technical for the introduction. I used "syntactic construction" and made appeal to the reader intuition by saying that such construction behaves similarly to a tactical. I think the text would be much more readable if "the tactics described in Chapter..." could be replaced by a *name*, but I'm afraid the only one I could use (Ltac) is a bit too ambiguous. So I'm open to suggestions. | |||
| 2017-08-02 | Rephrasing a couple of sentences in a more factual way. | Hugo Herbelin | |
| 2017-08-02 | Rephrasing the introduction in a more factual and up-to-date way. | Hugo Herbelin | |
| 2017-08-02 | Port ssr manual to Coq's latex/hevea style | Enrico Tassi | |
| Work done by Assia Mahboubi and Enrico Tassi | |||
| 2017-08-02 | Makefile.doc: implement serve-refman-8080 target | Enrico Tassi | |
| We make it so that, by default, the HTML reference manual looks like the one published online (same .css) and we provide a target to serve it locally (requires python). | |||
| 2017-08-02 | Update Setoid.tex | larsr | |
| The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`. | |||
| 2017-08-02 | Typo in the documentation of cumulativity | Amin Timany | |
| 2017-08-01 | Improve style slightly | Sam Pablo Kuper | |
| per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940). | |||
| 2017-08-01 | 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-07-31 | 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 | |
| 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 | |||
| 2017-07-31 | 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-29 | Drop paragraph mentioning Addendum as separate doc. | Théo Zimmermann | |
| As suggested by @herbelin. | |||
| 2017-07-28 | 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-27 | 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 | |
| Also includes a minor fix of the Extraction doc (a Require was missing). | |||
| 2017-07-27 | [toplevel] Remove long ago deprecated and NOOP options. | Emilio Jesus Gallego Arias | |
| Minor clean up, no sense in having these as they do nothing. | |||
| 2017-07-21 | Adding a V8.7 compatibility version number. | Hugo Herbelin | |
| 2017-07-20 | Merge branch 'v8.7' | Maxime Dénès | |
| 2017-07-19 | Merge PR #745: Add timing scripts | Maxime Dénès | |
| 2017-07-17 | Merge PR #865: RefMan-ext: fix some typos | Maxime Dénès | |
| 2017-07-14 | Update with non structurally recursive | william-lawvere | |
| 2017-07-11 | Sync the manual with the deprecation warnings. | Théo Zimmermann | |
| 2017-07-11 | Document the timing targets | Jason Gross | |
| We document the most useful timing targets and variables, how to invoke them, and what the output looks like. | |||
| 2017-07-11 | Strip trailing spaces | Jason Gross | |
| 2017-07-07 | 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |