aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Merge PR #823: Async off in Windows by default in CoqIDEGravatar Maxime Dénès2017-07-28
|\
* | Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
| |
* | Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \
| * \ Merge PR #745: Add timing scriptsGravatar Maxime Dénès2017-07-19
| |\ \
* | \ \ Merge PR #865: RefMan-ext: fix some typosGravatar Maxime Dénès2017-07-17
|\ \ \ \
| * | | | Update with non structurally recursiveGravatar william-lawvere2017-07-14
| | | | |
| | * | | Sync the manual with the deprecation warnings.Gravatar Théo Zimmermann2017-07-11
| |/ / / |/| | |
| | * | Document the timing targetsGravatar Jason Gross2017-07-11
| | | | | | | | | | | | | | | | | | | | We document the most useful timing targets and variables, how to invoke them, and what the output looks like.
| | * | Strip trailing spacesGravatar Jason Gross2017-07-11
| |/ / |/| |
| * | RefMan-ext: fix some typosGravatar William Lawvere2017-07-07
| | |
* | | Merge PR #842: Update the Tutorial.Gravatar Maxime Dénès2017-07-07
|\ \ \
* \ \ \ Merge PR #835: Remove doc/refman/RefMan-ind.texGravatar Maxime Dénès2017-07-07
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR #837: Add inversion_sigma to CHANGES and to docGravatar Maxime Dénès2017-07-05
|\ \ \ \
* \ \ \ \ Merge PR #850: Improve grammar in RefMan-Gal and RefMan-synGravatar Maxime Dénès2017-07-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #832: Document an example `Makefile` for `coq_makefile`Gravatar Maxime Dénès2017-07-05
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \ \ \ \ \ \
| | | * | | | | Update RefMan-syn.texGravatar william-lawvere2017-07-01
| | | | | | | |
| | | * | | | | Merge remote-tracking branch 'upstream/trunk' into trunkGravatar William Lawvere2017-07-01
| | | |\ \ \ \ \ | |_|_|/ / / / / |/| | | | | | |
| | | * | | | | RefMan-gal: improve grammarGravatar William Lawvere2017-07-01
| | | | | | | |
| | | * | | | | RefMan-syn: grammar editGravatar William Lawvere2017-07-01
| | | | | | | |
| | * | | | | | Document an example `Makefile` for `coq_makefile`Gravatar Jason Gross2017-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.texGravatar Jason Gross2017-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-tacGravatar Jason Gross2017-06-30
| |_|/ / / |/| | | |
| | | * | Mention again how to report bug and get version number.Gravatar Théo Zimmermann2017-06-30
| | | | | | | | | | | | | | | | | | | | As suggested by @psteckler.
| | | * | Better phrasing.Gravatar Théo Zimmermann2017-06-29
| | | | |
| | | * | More substance on discouraged practices.Gravatar Théo Zimmermann2017-06-29
| | | | |
| | | * | Some more corrections to the tutorial.Gravatar Théo Zimmermann2017-06-29
| | | | |
| | | * | Mask the reliance on coqtop.Gravatar Théo Zimmermann2017-06-29
| | | | |
| | | * | Update the Tutorial.Gravatar Théo Zimmermann2017-06-28
| |_|/ / |/| | |
| | | * disable async on Windows by defaultGravatar Paul Steckler2017-06-26
| |_|/ |/| |
| * | Merge PR#756: Fix Bug #5574, document function scopeGravatar Maxime Dénès2017-06-26
| |\ \
| | * | Fix Bug #5574, document function scopeGravatar Paul Steckler2017-06-23
| | | |
| * | | Merge PR#740: Refactor documentation of records.Gravatar Maxime Dénès2017-06-23
| |\ \ \
* | \ \ \ Merge PR#777: Improving documentation of tactic "move" (report #4561)Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \
| | | * | | Refactor documentation of records.Gravatar Théo Zimmermann2017-06-16
| | | |/ / | | | | | | | | | | | | | | | This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971
| | * | | Merge PR#767: Document named evars (including Show ident)Gravatar Maxime Dénès2017-06-16
| | |\ \ \
* | | | | | Document cumulativity for inductive typesGravatar Amin Timany2017-06-16
| | | | | |
* | | | | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#765: Remove obsolete Show commandsGravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \ \
* | | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-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 trunkGravatar William Lawvere2017-06-13
| | | | | | | |\ | |_|_|_|_|_|_|/ |/| | | | | | |
| | * | | | | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ / / / / / |/| | | | | |
| | | | | | * doc: improve grammar of RefMan-synGravatar William Lawvere2017-06-13
| | | | | | |
| | * | | | | Improving documentation of tactic "move" (report #4561).Gravatar Hugo Herbelin2017-06-13
| | | |_|_|/ | | |/| | |
* | / | | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-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.Gravatar Théo Zimmermann2017-06-13
| | | | |
| | | * | Document Show ident.Gravatar Théo Zimmermann2017-06-13
| | | | |
| | | * | Document evar naming syntax.Gravatar Théo Zimmermann2017-06-13
| | | |/
| * | / Remove commented documentation for Show Tree.Gravatar Théo Zimmermann2017-06-12
|/ / /
| * / Fix documentation of Typeclasses eauto :=Gravatar Théo Zimmermann2017-06-07
| |/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 14:38:11 +0000