Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #823: Async off in Windows by default in CoqIDE | 2017-07-28 | |
|\ | |||
* | | Adding a V8.7 compatibility version number. | 2017-07-21 | |
| | | |||
* | | Merge branch 'v8.7' | 2017-07-20 | |
|\ \ | |||
| * \ | Merge PR #745: Add timing scripts | 2017-07-19 | |
| |\ \ | |||
* | \ \ | Merge PR #865: RefMan-ext: fix some typos | 2017-07-17 | |
|\ \ \ \ | |||
| * | | | | Update with non structurally recursive | 2017-07-14 | |
| | | | | | |||
| | * | | | Sync the manual with the deprecation warnings. | 2017-07-11 | |
| |/ / / |/| | | | |||
| | * | | Document the timing targets | 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 | 2017-07-11 | |
| |/ / |/| | | |||
| * | | RefMan-ext: fix some typos | 2017-07-07 | |
| | | | |||
* | | | Merge PR #842: Update the Tutorial. | 2017-07-07 | |
|\ \ \ | |||
* \ \ \ | Merge PR #835: Remove doc/refman/RefMan-ind.tex | 2017-07-07 | |
|\ \ \ \ | |_|/ / |/| | | | |||
* | | | | Merge PR #837: Add inversion_sigma to CHANGES and to doc | 2017-07-05 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn | 2017-07-05 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #832: Document an example `Makefile` for `coq_makefile` | 2017-07-05 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge branch 'v8.6' | 2017-07-04 | |
|\ \ \ \ \ \ \ | |||
| | | * | | | | | Update RefMan-syn.tex | 2017-07-01 | |
| | | | | | | | | |||
| | | * | | | | | Merge remote-tracking branch 'upstream/trunk' into trunk | 2017-07-01 | |
| | | |\ \ \ \ \ | |_|_|/ / / / / |/| | | | | | | | |||
| | | * | | | | | RefMan-gal: improve grammar | 2017-07-01 | |
| | | | | | | | | |||
| | | * | | | | | RefMan-syn: grammar edit | 2017-07-01 | |
| | | | | | | | | |||
| | * | | | | | | Document an example `Makefile` for `coq_makefile` | 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 | 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 | 2017-06-30 | |
| |_|/ / / |/| | | | | |||
| | | * | | Mention again how to report bug and get version number. | 2017-06-30 | |
| | | | | | | | | | | | | | | | | | | | | As suggested by @psteckler. | ||
| | | * | | Better phrasing. | 2017-06-29 | |
| | | | | | |||
| | | * | | More substance on discouraged practices. | 2017-06-29 | |
| | | | | | |||
| | | * | | Some more corrections to the tutorial. | 2017-06-29 | |
| | | | | | |||
| | | * | | Mask the reliance on coqtop. | 2017-06-29 | |
| | | | | | |||
| | | * | | Update the Tutorial. | 2017-06-28 | |
| |_|/ / |/| | | | |||
| | | * | disable async on Windows by default | 2017-06-26 | |
| |_|/ |/| | | |||
| * | | Merge PR#756: Fix Bug #5574, document function scope | 2017-06-26 | |
| |\ \ | |||
| | * | | Fix Bug #5574, document function scope | 2017-06-23 | |
| | | | | |||
| * | | | Merge PR#740: Refactor documentation of records. | 2017-06-23 | |
| |\ \ \ | |||
* | \ \ \ | Merge PR#777: Improving documentation of tactic "move" (report #4561) | 2017-06-19 | |
|\ \ \ \ \ | |||
| | | * | | | Refactor documentation of records. | 2017-06-16 | |
| | | |/ / | | | | | | | | | | | | | | | | This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971 | ||
| | * | | | Merge PR#767: Document named evars (including Show ident) | 2017-06-16 | |
| | |\ \ \ | |||
* | | | | | | Document cumulativity for inductive types | 2017-06-16 | |
| | | | | | | |||
* | | | | | | Merge PR#375: Deprecation | 2017-06-15 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR#765: Remove obsolete Show commands | 2017-06-14 | |
|\ \ \ \ \ \ \ | |||
* | | | | | | | | Prelude : no more autoload of plugins extraction and recdef | 2017-06-14 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
| | | | | | | * | Merge remote-tracking branch 'upstream/trunk' into trunk | 2017-06-13 | |
| | | | | | | |\ | |_|_|_|_|_|_|/ |/| | | | | | | | |||
| | * | | | | | | Remove support for Coq 8.4. | 2017-06-14 | |
| |/ / / / / / |/| | | | | | | |||
| | | | | | * | doc: improve grammar of RefMan-syn | 2017-06-13 | |
| | | | | | | | |||
| | * | | | | | Improving documentation of tactic "move" (report #4561). | 2017-06-13 | |
| | | |_|_|/ | | |/| | | | |||
* | / | | | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | 2017-06-13 | |
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude. | ||
| | | * | | Document instantiate (ident := term) and make it the preferred variant. | 2017-06-13 | |
| | | | | | |||
| | | * | | Document Show ident. | 2017-06-13 | |
| | | | | | |||
| | | * | | Document evar naming syntax. | 2017-06-13 | |
| | | |/ | |||
| * | / | Remove commented documentation for Show Tree. | 2017-06-12 | |
|/ / / | |||
| * / | Fix documentation of Typeclasses eauto := | 2017-06-07 | |
| |/ |