aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Add doc for Set Debug Cbv.Gravatar Gaëtan Gilbert2017-12-14
* Add doc for Set Info/Debug Auto/Trivial/Eauto.Gravatar Gaëtan Gilbert2017-12-14
* Add optindex for Set Bullet Behavior.Gravatar Gaëtan Gilbert2017-12-14
* Add doc for Set Congruence VerboseGravatar Gaëtan Gilbert2017-12-14
* Fix typo in doc optindex for Typeclass Resolution ...Gravatar Gaëtan Gilbert2017-12-14
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | Updating the current official writing of OCaml, updating Camlp4->Camlp5.Gravatar Hugo Herbelin2017-11-25
| * Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
|/
* 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
| |/ |/|
| * 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
| |_|/ / |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 22:38:11 +0000