| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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 | |
| 2017-06-13 | doc: improve grammar of RefMan-syn | William Lawvere | |
| 2017-06-13 | Improving documentation of tactic "move" (report #4561). | Hugo Herbelin | |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | |
| 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. | |||
| 2017-06-13 | Document instantiate (ident := term) and make it the preferred variant. | Théo Zimmermann | |
| 2017-06-13 | Document Show ident. | Théo Zimmermann | |
| 2017-06-13 | Document evar naming syntax. | Théo Zimmermann | |
| 2017-06-12 | Remove commented documentation for Show Tree. | Théo Zimmermann | |
| 2017-06-07 | Fix documentation of Typeclasses eauto := | Théo Zimmermann | |
| 2017-06-01 | Merge PR#449: make specialize smarter (bug 5370). | Maxime Dénès | |
| 2017-05-31 | Documenting the new behaviour of specialize. | Pierre Courtieu | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |