aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Collapse)Author
2018-09-20[doc] Move the LaTeX preamble to a separate .tex fileClément Pit-Claudel
2018-09-20[doc] Fix a typo in coqdomain.pyClément Pit-Claudel
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines.
2018-07-26[sphinx] Do name cleanup in handle_signatureClément Pit-Claudel
2018-07-25[sphinx] Add a way of skipping names in the indexes.Théo Zimmermann
2018-06-21Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵Maxime Dénès
understands.
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
It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.
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
As discussed in GH-7556.
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
Co-Authored-By: @Zimmi48
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
Co-Authored-By: @Zimmi48
2018-05-15[doc] Add a README to doc/sphinx/Clément Pit-Claudel
The readme is auto-generated by combining introductory text with the docstrings in coqdomain.py.
2018-05-15[doc] Document all directives and roles of our Sphinx domainClément Pit-Claudel
Also get rid of a few unused or redundant constructs: the :ltac: role and the 'tac' directive (unused) and the :gallina: and :notation: roles (redundant).
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
The Ubuntu Font License requires substantially modified fonts to be renamed entirely.
2018-04-14[Sphinx] Add chapter 9.Théo Zimmermann
Chapter ported by Théo Zimmermann and Maxime Dénès.
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
Code from Paul Steckler (MIT).
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
The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content.
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
2015-10-13Fix some typos.Guillaume Melquiond
2014-08-25"allows to", like "allowing to", is improperJason Gross
It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
2010-09-19Hopefully a fix for #2176 (redirection not understood with some shells)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-21Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824herbelin
from v8.2 branch]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11825 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19Propriétés svn pour les filtres latexnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11807 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Backporting from v8.2 to trunk:herbelin
- Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin
principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 22:26:08 +0000