| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-31 | Merge PR #993: Credits for version 8.7 | Maxime Dénès | |
| 2017-08-31 | Credits for version 8.7 | Matthieu Sozeau | |
| 2017-08-31 | Merge PR #958: coq_makefile: build/use .cma for packed plugins too | Maxime Dénès | |
| 2017-08-29 | coq_makefile: improve documentation | Enrico Tassi | |
| 2017-08-29 | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès | |
| 2017-08-29 | Merge PR #988: Fix obsolete description of real numerals. | Maxime Dénès | |
| 2017-08-29 | Merge PR #819: Cleanup old things | Maxime Dénès | |
| 2017-08-29 | Merge PR #773: [flags] Remove XML output flag. | Maxime Dénès | |
| 2017-08-23 | Update coypright dates on documentation | Matthieu Sozeau | |
| 2017-08-22 | Fix obsolete description of real numerals. | Guillaume Melquiond | |
| 2017-08-18 | use OCaml temp_file, instead of our own version | Paul Steckler | |
| 2017-08-18 | Merge PR #973: Adding documentation for Printing Focused option. | Maxime Dénès | |
| 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-17 | Adding documentation for Printing Focused option. | Pierre Courtieu | |
| 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 | Unbreak RecTutorial.v | Gaëtan Gilbert | |
| The RecTutorial.tex still contains similarly broken Coq code, it just doesn't run it. | |||
| 2017-08-01 | Remove old doc/rt files. | Gaëtan Gilbert | |
| 2017-08-01 | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | |
| This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |