aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Merge PR #933: Fix documentation of Hint Mode (bug #4911).Gravatar Maxime Dénès2017-08-01
|\
* \ Merge PR #932: Fix shuffled documentation.Gravatar Maxime Dénès2017-08-01
|\ \
* \ \ Merge PR #929: Add missing paragraph to introductionGravatar Maxime Dénès2017-08-01
|\ \ \
* \ \ \ Merge PR #925: Document Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\ \ \ \
* \ \ \ \ Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \
| | | * | | Drop paragraph mentioning Addendum as separate doc.Gravatar Théo Zimmermann2017-07-29
* | | | | | Merge PR #823: Async off in Windows by default in CoqIDEGravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \
| | | | | | * Fix documentation of Hint Mode (bug #4911).Gravatar Guillaume Melquiond2017-07-28
| |_|_|_|_|/ |/| | | | |
| | | | | * Fix shuffled documentation.Gravatar Guillaume Melquiond2017-07-28
| |_|_|_|/ |/| | | |
| | | | * Add missing paragraph to introductionGravatar Benjamin Pierce2017-07-27
| |_|_|/ |/| | |
| | | * Extraction.tex: mention the possible "From Coq Require Extraction"Gravatar letouzey2017-07-27
| | | * Extraction TestCompile documented + mentionned in CHANGESGravatar Pierre Letouzey2017-07-27
| |_|/ |/| |
| | * [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |/ |/|
* | 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
| | * | 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
| |/ / / / / / |/| | | | | |
| | | | * | | Remove doc/refman/RefMan-ind.texGravatar Jason Gross2017-06-30
| |_|_|/ / / |/| | | | |
| | | * | | 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
| | | * | 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
| | | |/ /
| | * | | 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
|\ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 07:33:51 +0000