aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Expand)Author
2018-06-21Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understa...Maxime Dénès
2018-06-20On cygwin, pass the filename in a format that coqdoc understands.Jim Fehrle
2018-06-19[doc] Rewrite and document the prodn directiveClément Pit-Claudel
2018-06-08gitlab: build sphinx doc in separate jobGaëtan Gilbert
2018-05-25[doc] Allow more than one signature and name per Sphinx objectClément Pit-Claudel
2018-05-25Merge PR #7556: Add a setting to warn about empty object in the refmanMaxime Dénès
2018-05-22[doc] Add a setting to warn about empty Coq objectsClément Pit-Claudel
2018-05-16[sphinx] Bump timeout. Closes #7532.Clément Pit-Claudel
2018-05-15[doc] More feedback on doc writer guideClément Pit-Claudel
2018-05-15[doc] Search for 'coqtop' in $PATH if COQBIN is unsetClément Pit-Claudel
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
2018-05-15[doc] Add a README to doc/sphinx/Clément Pit-Claudel
2018-05-15[doc] Document all directives and roles of our Sphinx domainClément Pit-Claudel
2018-05-15[doc] Compute the path to coqdoc at run time, not at load timeClément Pit-Claudel
2018-05-09[sphinx] Warn for dangling tacn / cmd / opt / ... references.Clément Pit-Claudel
2018-04-16Merge PR #7251: doc: Rename UbuntuMono-Square to CoqNotations and tweak spacingMaxime Dénès
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14doc: Rename UbuntuMono-Square to CoqNotations and tweak spacingClément Pit-Claudel
2018-04-14[Sphinx] Add chapter 9.Théo Zimmermann
2018-04-09[Sphinx] Make it possible to espace { by %{ in custom grammarsMaxime Dénès
2018-03-16[Sphinx] Better error message for coqtop errorsMaxime Dénès
2018-03-16[Sphinx] Increase coqtop timeout to avoid spurious failures on CIMaxime Dénès
2018-03-12[Sphinx] Add a few grammar constructionsMaxime Dénès
2018-03-09Moving Gitlab CI documentation build to the main Coq build.Maxime Dénès
2018-03-09Integration of a sphinx-based documentation generator.Maxime Dénès
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2015-10-13Fix some typos.Guillaume Melquiond
2014-08-25"allows to", like "allowing to", is improperJason Gross
2010-09-19Hopefully a fix for #2176 (redirection not understood with some shells)herbelin
2009-01-21Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824herbelin
2009-01-19Propriétés svn pour les filtres latexnotin
2009-01-18Backporting from v8.2 to trunk:herbelin
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:22:46 +0000