aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Merge PR #993: Credits for version 8.7Gravatar Maxime Dénès2017-08-31
|\
| * Credits for version 8.7Gravatar Matthieu Sozeau2017-08-31
* | Merge PR #958: coq_makefile: build/use .cma for packed plugins tooGravatar Maxime Dénès2017-08-31
|\ \
| * | coq_makefile: improve documentationGravatar Enrico Tassi2017-08-29
* | | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\ \ \
* \ \ \ Merge PR #988: Fix obsolete description of real numerals.Gravatar Maxime Dénès2017-08-29
|\ \ \ \
* \ \ \ \ Merge PR #819: Cleanup old thingsGravatar Maxime Dénès2017-08-29
|\ \ \ \ \
* \ \ \ \ \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | | | | * Update coypright dates on documentationGravatar Matthieu Sozeau2017-08-23
| |_|_|_|/ |/| | | |
| | | * | Fix obsolete description of real numerals.Gravatar Guillaume Melquiond2017-08-22
| |_|/ / |/| | |
| | | * use OCaml temp_file, instead of our own versionGravatar Paul Steckler2017-08-18
* | | | Merge PR #973: Adding documentation for Printing Focused option.Gravatar Maxime Dénès2017-08-18
|\ \ \ \
| | | | * Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
| |_|_|/ |/| | |
* | | | Merge PR #974: Change section caption, improve some wordingGravatar Maxime Dénès2017-08-17
|\ \ \ \
* | | | | Document anonymous universes (PR #544).Gravatar Gaëtan Gilbert2017-08-17
| | * | | Adding documentation for Printing Focused option.Gravatar Pierre Courtieu2017-08-17
| |/ / / |/| | |
| * | | mention that tactic is the identity or gives errorGravatar Paul Steckler2017-08-16
| * | | change section caption, improve some wordingGravatar Paul Steckler2017-08-16
|/ / /
* | | Merge PR #831: Port ssreflect user manual to Coq's latex/hevea styleGravatar Maxime Dénès2017-08-16
|\ \ \
* \ \ \ Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)Gravatar Maxime Dénès2017-08-16
|\ \ \ \
* \ \ \ \ Merge PR #943: Reference Manual: minor wording improvementsGravatar Maxime Dénès2017-08-16
|\ \ \ \ \
* \ \ \ \ \ Merge PR #940: Replace jarring use of "Remark" with "Note"Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #934: Fix some coq-tex errors in the reference manual.Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \
| | | | | | * | | Rewording the introductionGravatar Enrico Tassi2017-08-02
| | | | | | * | | Rephrasing a couple of sentences in a more factual way.Gravatar Hugo Herbelin2017-08-02
| | | | | | * | | Rephrasing the introduction in a more factual and up-to-date way.Gravatar Hugo Herbelin2017-08-02
| | | | | | * | | Port ssr manual to Coq's latex/hevea styleGravatar Enrico Tassi2017-08-02
| | | | | | * | | Makefile.doc: implement serve-refman-8080 targetGravatar Enrico Tassi2017-08-02
| |_|_|_|_|/ / / |/| | | | | | |
| | | | | * | | Update Setoid.texGravatar larsr2017-08-02
| |_|_|_|/ / / |/| | | | | |
| * | | | | | Typo in the documentation of cumulativityGravatar Amin Timany2017-08-02
| | | | | | * Unbreak RecTutorial.vGravatar Gaëtan Gilbert2017-08-01
| | | | | | * Remove old doc/rt files.Gravatar Gaëtan Gilbert2017-08-01
| |_|_|_|_|/ |/| | | | |
| | | | | * [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |_|_|_|/ |/| | | |
| | | * | Improve style slightlyGravatar Sam Pablo Kuper2017-08-01
* | | | | 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
|\ \ \ \ \ \ \ \ \
| | | | | | | | | * Fix incorrect use of "At the end".Gravatar Sam Pablo Kuper2017-07-31
| | | | | | | | | * Minor grammar fix: replace a "then" with a "so".Gravatar Sam Pablo Kuper2017-07-31
| |_|_|_|_|_|_|_|/ |/| | | | | | | |
| | | | | | | | * Replace jarring use of "Remark" with "Note"Gravatar Sam Pablo Kuper2017-07-31
| |_|_|_|_|_|_|/ |/| | | | | | |
| | | | | | * | Update documentation of cumulativityGravatar Amin Timany2017-07-31
| | | | | | * | Fix typo and Add Jason's example to the docGravatar Amin Timany2017-07-31
| | | | | | * | Improve documentation of cumulativityGravatar Amin Timany2017-07-31
| |_|_|_|_|/ / |/| | | | | |
| | | * | | | 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 some coq-tex errors in the reference manual.Gravatar Guillaume Melquiond2017-07-28
| |_|_|_|_|_|/ |/| | | | | |
| | | | | | * Fix documentation of Hint Mode (bug #4911).Gravatar Guillaume Melquiond2017-07-28
| |_|_|_|_|/ |/| | | | |