| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-28 | Merge PR #823: Async off in Windows by default in CoqIDE | Maxime Dénès | |
| 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 #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-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-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 | doc: improve grammar of RefMan-syn | William Lawvere | |
| 2017-06-13 | Improving documentation of tactic "move" (report #4561). | Hugo Herbelin | |
| 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 | |
| 2017-05-30 | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin | |
| Includes fixes and suggestions from Théo. | |||
| 2017-05-27 | Documenting the existence of first and solve as Ltac definitions. | Pierre-Marie Pédrot | |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès | |
| 2017-05-23 | add the only target | Enrico Tassi | |
| This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think | |||
| 2017-05-23 | enters coq_makefile2 | Enrico Tassi | |
| 2017-05-23 | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | |
| We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc... | |||
| 2017-05-23 | [vernac] Remove `Save.` command. | Emilio Jesus Gallego Arias | |
| It has been deprecated for a while in favor of `Qed`. | |||
| 2017-05-17 | Documenting relaxing of constraints on injection. | Hugo Herbelin | |
| We seized this opportunity to do a little refreshing of the section describing injection. | |||
| 2017-05-17 | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | |
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |