aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools
Commit message (Expand)AuthorAge
* gitlab: build sphinx doc in separate jobGravatar Gaëtan Gilbert2018-06-08
* [doc] Allow more than one signature and name per Sphinx objectGravatar Clément Pit-Claudel2018-05-25
* Merge PR #7556: Add a setting to warn about empty object in the refmanGravatar Maxime Dénès2018-05-25
|\
| * [doc] Add a setting to warn about empty Coq objectsGravatar Clément Pit-Claudel2018-05-22
* | [sphinx] Bump timeout. Closes #7532.Gravatar Clément Pit-Claudel2018-05-16
|/
* [doc] More feedback on doc writer guideGravatar Clément Pit-Claudel2018-05-15
* [doc] Search for 'coqtop' in $PATH if COQBIN is unsetGravatar Clément Pit-Claudel2018-05-15
* [doc] Address feedback on doc writer guideGravatar Clément Pit-Claudel2018-05-15
* [doc] Add a README to doc/sphinx/Gravatar Clément Pit-Claudel2018-05-15
* [doc] Document all directives and roles of our Sphinx domainGravatar Clément Pit-Claudel2018-05-15
* [doc] Compute the path to coqdoc at run time, not at load timeGravatar Clément Pit-Claudel2018-05-15
* [sphinx] Warn for dangling tacn / cmd / opt / ... references.Gravatar Clément Pit-Claudel2018-05-09
* Merge PR #7251: doc: Rename UbuntuMono-Square to CoqNotations and tweak spacingGravatar Maxime Dénès2018-04-16
|\
* | [Sphinx] Fix all remaining warnings.Gravatar Maxime Dénès2018-04-14
| * doc: Rename UbuntuMono-Square to CoqNotations and tweak spacingGravatar Clément Pit-Claudel2018-04-14
* | [Sphinx] Add chapter 9.Gravatar Théo Zimmermann2018-04-14
* | [Sphinx] Make it possible to espace { by %{ in custom grammarsGravatar Maxime Dénès2018-04-09
|/
* [Sphinx] Better error message for coqtop errorsGravatar Maxime Dénès2018-03-16
* [Sphinx] Increase coqtop timeout to avoid spurious failures on CIGravatar Maxime Dénès2018-03-16
* [Sphinx] Add a few grammar constructionsGravatar Maxime Dénès2018-03-12
* Moving Gitlab CI documentation build to the main Coq build.Gravatar Maxime Dénès2018-03-09
* Integration of a sphinx-based documentation generator.Gravatar Maxime Dénès2018-03-09
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Hopefully a fix for #2176 (redirection not understood with some shells)Gravatar herbelin2010-09-19
* Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824Gravatar herbelin2009-01-21
* Propriétés svn pour les filtres latexGravatar notin2009-01-19
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23