| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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-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 | |
| 2017-07-05 | 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-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-01 | 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-06-30 | Document an example `Makefile` for `coq_makefile` | Jason Gross | |
| We document an example `Makefile` which does not include the generated `CoqMakefile`, but instead invokes arbitrary targets in it. | |||
| 2017-06-30 | Remove doc/refman/RefMan-ind.tex | Jason Gross | |
| It does not seem to be referred to by any file, and does not seem to be built by any implicit rules. | |||
| 2017-06-30 | Add doc for inversion_sigma to RefMan-tac | Jason Gross | |
| 2017-06-30 | Mention again how to report bug and get version number. | Théo Zimmermann | |
| As suggested by @psteckler. | |||
| 2017-06-29 | Better phrasing. | Théo Zimmermann | |
| 2017-06-29 | More substance on discouraged practices. | Théo Zimmermann | |
| 2017-06-29 | Some more corrections to the tutorial. | Théo Zimmermann | |
| 2017-06-29 | Mask the reliance on coqtop. | Théo Zimmermann | |
| 2017-06-28 | Update the Tutorial. | Théo Zimmermann | |
| 2017-06-26 | disable async on Windows by default | Paul Steckler | |
| 2017-06-26 | Merge PR#756: Fix Bug #5574, document function scope | Maxime Dénès | |
| 2017-06-23 | Fix Bug #5574, document function scope | Paul Steckler | |
| 2017-06-23 | Merge PR#740: Refactor documentation of records. | Maxime Dénès | |
| 2017-06-19 | Merge PR#777: Improving documentation of tactic "move" (report #4561) | Maxime Dénès | |
| 2017-06-16 | Refactor documentation of records. | Théo Zimmermann | |
| This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971 | |||
| 2017-06-16 | Merge PR#767: Document named evars (including Show ident) | Maxime Dénès | |
| 2017-06-16 | Document cumulativity for inductive types | Amin Timany | |
| 2017-06-15 | Merge PR#375: Deprecation | Maxime Dénès | |
| 2017-06-14 | Merge PR#765: Remove obsolete Show commands | Maxime Dénès | |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | |
| The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. | |||
| 2017-06-13 | Merge remote-tracking branch 'upstream/trunk' into trunk | William Lawvere | |
| 2017-06-14 | Remove support for Coq 8.4. | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |