| Commit message (Collapse) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | | | | | | * | | 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 | 2017-08-02 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Work done by Assia Mahboubi and Enrico Tassi | |||
| | | | | | | | | | | | * | | Makefile.doc: implement serve-refman-8080 target | Enrico Tassi | 2017-08-02 | |
| | |_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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). | |||
| | | | | | | | * | | | | | Update Setoid.tex |  larsr | 2017-08-02 | |
| | |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`. | |||
| * | | | | | | | | | | | Makefile: 'make clean' now immune to the check for binary files without sources |  Pierre Letouzey | 2017-08-02 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a followup of 7d1fc15. Without this fix, you're warned of leftover files, but even a 'make clean' is then refused, so you cannot get rid of them easily (apart via a git clean -xfd). | |||
| | * | | | | | | | | | | Typo in the documentation of cumulativity |  Amin Timany | 2017-08-02 | |
| | | | | | | | | | | | | ||||
| | | | | | | | | | * | | Printing goals does not evar-normalizes beforehand anymore. |  Pierre-Marie Pédrot | 2017-08-01 | |
| | | | | | | | | | | | | ||||
| | | | | | | | | | * | | Detyping functions are now operating on EConstr.t. | Pierre-Marie Pédrot | 2017-08-01 | |
| | |_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was already the case, but the API was not exposing this. | |||
| | | | | | | * | | | | Fix typos. Improve wording. |  Sam Pablo Kuper | 2017-08-01 | |
| | | | | | | | | | | | ||||
| | | | | * | | | | | | 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 #928: Fixing bug #5671 (tactic specialize unclean wrt Metas). | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #926: test-suite uses Extraction TestCompile | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #925: Document Extraction TestCompile | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #921: [make] remove compat5 file. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #917: Moving --print-version to -print-version for consistency. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #913: Less allocations in Detyping | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709) | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND. | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵ | Maxime Dénès | 2017-08-01 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | y , z". | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #806: closing bug 5315 | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | | | | | | * | | adding a comment to explain the change |  Julien Forest | 2017-08-01 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | | | * | | solving b1859 | Julien Forest | 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 | |
| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | Improve errors for cumulativity when monomorphic | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic. | |||
| | | | | | | | | | | | | | | | | * | | | | | | Change the option for 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 | |
| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | Add Jason's example of fun-ext with cumulativity | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | Add test for NonCumulative inductives | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | Issue error on monomorphic cumulative inductives | Amin Timany | 2017-07-31 | |
| | | | | | | | | | | | | | | | | | |_|/ / / | | | | | | | | | | | | | | | | |/| | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | 2017-07-31 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #746: Timing on ci via coq_makefile for various projects | Maxime Dénès | 2017-07-31 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | * | | | | | | | Drop paragraph mentioning Addendum as separate doc. |  Théo Zimmermann | 2017-07-29 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As suggested by @herbelin. | |||
| | | | | * | | | | | | | | | | | | | | | | | | closing bug 5315 |  Julien Forest | 2017-07-29 | |
| | |_|_|/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | Merge PR #923: [api] Fix base_include LTAC parts. | Maxime Dénès | 2017-07-28 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #889: Removing template polymorphism for definitions. | Maxime Dénès | 2017-07-28 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #888: Stronger kernel types | Maxime Dénès | 2017-07-28 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #823: Async off in Windows by default in CoqIDE | Maxime Dénès | 2017-07-28 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #782: Update API for fiat | 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 | |
| | | | | | | | | | | | | | | | | | | | | |/ / / / | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |