aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Collapse)Author
2018-10-15Correct some spelling errorsBenjamin Barenblat
Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
2018-10-01Merge PR #8301: Documentation for proof diffsThéo Zimmermann
2018-09-25[doc] Fix GH-8529: wrap macro definitions in math delimiters for MathJaxClément Pit-Claudel
2018-09-23Update flag, option and table descriptions in coqdomain.py, update ↵Jim Fehrle
README.rst to match. Bump env_version.
2018-09-23Documentation for proof diffsJim Fehrle
2018-09-20Define flags (binary-valued settings) and tables (settings that are sets)Jim Fehrle
as separate NotationObject types, include in index.
2018-09-20[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-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979Clément Pit-Claudel
2018-09-20[doc] Ensure that merging coqtop blocks preserves anchorsClément Pit-Claudel
2018-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4980Clément Pit-Claudel
2018-09-20[doc] Fix a typo in the developer guideClément Pit-Claudel
2018-09-20[doc] Add env_version to metadata of coqrst pluginClément Pit-Claudel
This is required by Sphinx 8.0. See https://github.com/sphinx-doc/sphinx/issues/4460.
2018-09-20[doc] Create a separate index file for the LaTeX buildClément Pit-Claudel
See https://github.com/sphinx-doc/sphinx/issues/4977 for context.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:21:57 +0000