aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
...
| * | use OCaml criteria for infix ops, #6212Gravatar Paul Steckler2017-11-22
|/ /
* | Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gravatar Gaëtan Gilbert2017-11-19
* | coq_makefile: document COQ_SRC_SUBDIRSGravatar Enrico Tassi2017-11-13
* | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Gravatar Samuel Gruetter2017-11-06
* | Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\ \
* \ \ Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631Gravatar Maxime Dénès2017-10-27
|\ \ \
* | | | Rename \Tree to \NatTreeGravatar Johannes Kloos2017-10-25
| | * | Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
* | | | Fix #5763: Strictly positive example is out of order.Gravatar jkloos2017-10-24
| * | | Fix #4846Gravatar Johannes Kloos2017-10-24
| * | | Fix #5413: [unfold ... in] not documentedGravatar Johannes Kloos2017-10-24
| * | | Documentation: Add various basic constructs to the index.Gravatar Johannes Kloos2017-10-24
| * | | Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Gravatar Johannes Kloos2017-10-24
|/ / /
* | | Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
* | | Merge PR #1116: Updating citing Coq in FAQ.Gravatar Maxime Dénès2017-10-10
|\ \ \ | |/ / |/| |
| * | Updating citing Coq in FAQ.Gravatar Hugo Herbelin2017-10-10
* | | Fix copyright info in reference manual.Gravatar Théo Zimmermann2017-10-06
* | | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Gravatar Maxime Dénès2017-10-05
|\ \ \
* \ \ \ Merge PR #1080: Remove some unused parts of the reference manual.Gravatar Maxime Dénès2017-10-03
|\ \ \ \
* | | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| |_|/ / |/| | |
| * | | Remove some unused parts of the reference manual.Gravatar Guillaume Melquiond2017-09-22
* | | | Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
|/ / /
| * / Reference manual: A few words about the file system constraints for -Q/-R.Gravatar Hugo Herbelin2017-09-13
|/ /
* | Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Gravatar Maxime Dénès2017-09-11
|\ \
* \ \ Merge PR #1035: Fix the introduction of SSR refman chapter.Gravatar Maxime Dénès2017-09-11
|\ \ \
* \ \ \ Merge PR #1014: Add option index entry for NativeCompute ProfilingGravatar Maxime Dénès2017-09-11
|\ \ \ \
* \ \ \ \ Merge PR #1004: Document primitive projections in more detailGravatar Maxime Dénès2017-09-11
|\ \ \ \ \
| | | | * | Fix Typo in Doc for `Set Parsing Explicit`Gravatar staffehn2017-09-08
| |_|_|/ / |/| | | |
| | | * | Fix the introduction of SSR refman chapter.Gravatar Théo Zimmermann2017-09-08
| |_|/ / |/| | |
* | | | 2 Typos in 'Add Parametric Morphism' DocumentationGravatar staffehn2017-09-03
| | * | add option index entry for NativeCompute ProfilingGravatar Paul Steckler2017-09-01
| |/ / |/| |
| | * Fixing various typos in the Credits chapter.Gravatar Théo Zimmermann2017-09-01
| |/ |/|
| * Document primitive projections in more detailGravatar Matthieu Sozeau2017-08-31
| * RefMan-ssr: fix warningGravatar Matthieu Sozeau2017-08-31
* | 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
| |/ / / |/| | |