aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tools
Commit message (Collapse)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
| | | | | | | | | | 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`.
* Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵Gravatar Maxime Dénès2018-06-21
|\ | | | | | | understands.
| * On cygwin, pass the filename in a format that coqdoc understands.Gravatar Jim Fehrle2018-06-20
| |
* | [doc] Rewrite and document the prodn directiveGravatar Clément Pit-Claudel2018-06-19
|/ | | | | 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.
* 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
| | | | As discussed in GH-7556.
* 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
| | | | Co-Authored-By: @Zimmi48
* [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
| | | | Co-Authored-By: @Zimmi48
* [doc] Add a README to doc/sphinx/Gravatar Clément Pit-Claudel2018-05-15
| | | | | The readme is auto-generated by combining introductory text with the docstrings in coqdomain.py.
* [doc] Document all directives and roles of our Sphinx domainGravatar Clément Pit-Claudel2018-05-15
| | | | | 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).
* [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
| | | | | | | | | | The Ubuntu Font License requires substantially modified fonts to be renamed entirely.
* | [Sphinx] Add chapter 9.Gravatar Théo Zimmermann2018-04-14
| | | | | | | | Chapter ported by Théo Zimmermann and Maxime Dénès.
* | [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
| | | | Code from Paul Steckler (MIT).
* 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
| | | | | | | | 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.
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| | | | | | | | 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.
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
|
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | 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).
* Hopefully a fix for #2176 (redirection not understood with some shells)Gravatar herbelin2010-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824Gravatar herbelin2009-01-21
| | | | | | | | from v8.2 branch]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propriétés svn pour les filtres latexGravatar notin2009-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - 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
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23
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.39.1) at 2024-05-16 03:45:18 +0000