Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵ | Maxime Dénès | 2018-06-21 |
|\ | | | | | | | understands. | ||
| * | On cygwin, pass the filename in a format that coqdoc understands. | Jim Fehrle | 2018-06-20 |
| | | |||
* | | [doc] Rewrite and document the prodn directive | Clément Pit-Claudel | 2018-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 job | Gaëtan Gilbert | 2018-06-08 |
| | |||
* | [doc] Allow more than one signature and name per Sphinx object | Clément Pit-Claudel | 2018-05-25 |
| | | | | As discussed in GH-7556. | ||
* | Merge PR #7556: Add a setting to warn about empty object in the refman | Maxime Dénès | 2018-05-25 |
|\ | |||
| * | [doc] Add a setting to warn about empty Coq objects | Clément Pit-Claudel | 2018-05-22 |
| | | |||
* | | [sphinx] Bump timeout. Closes #7532. | Clément Pit-Claudel | 2018-05-16 |
|/ | |||
* | [doc] More feedback on doc writer guide | Clément Pit-Claudel | 2018-05-15 |
| | | | | Co-Authored-By: @Zimmi48 | ||
* | [doc] Search for 'coqtop' in $PATH if COQBIN is unset | Clément Pit-Claudel | 2018-05-15 |
| | |||
* | [doc] Address feedback on doc writer guide | Clément Pit-Claudel | 2018-05-15 |
| | | | | Co-Authored-By: @Zimmi48 | ||
* | [doc] Add a README to doc/sphinx/ | Clément Pit-Claudel | 2018-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 domain | Clément Pit-Claudel | 2018-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 time | Clément Pit-Claudel | 2018-05-15 |
| | |||
* | [sphinx] Warn for dangling tacn / cmd / opt / ... references. | Clément Pit-Claudel | 2018-05-09 |
| | |||
* | Merge PR #7251: doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing | Maxime Dénès | 2018-04-16 |
|\ | |||
* | | [Sphinx] Fix all remaining warnings. | Maxime Dénès | 2018-04-14 |
| | | |||
| * | doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing | Clément Pit-Claudel | 2018-04-14 |
| | | | | | | | | | | The Ubuntu Font License requires substantially modified fonts to be renamed entirely. | ||
* | | [Sphinx] Add chapter 9. | Théo Zimmermann | 2018-04-14 |
| | | | | | | | | Chapter ported by Théo Zimmermann and Maxime Dénès. | ||
* | | [Sphinx] Make it possible to espace { by %{ in custom grammars | Maxime Dénès | 2018-04-09 |
|/ | |||
* | [Sphinx] Better error message for coqtop errors | Maxime Dénès | 2018-03-16 |
| | |||
* | [Sphinx] Increase coqtop timeout to avoid spurious failures on CI | Maxime Dénès | 2018-03-16 |
| | |||
* | [Sphinx] Add a few grammar constructions | Maxime Dénès | 2018-03-12 |
| | | | | Code from Paul Steckler (MIT). | ||
* | Moving Gitlab CI documentation build to the main Coq build. | Maxime Dénès | 2018-03-09 |
| | |||
* | Integration of a sphinx-based documentation generator. | Maxime Dénès | 2018-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. | Emilio Jesus Gallego Arias | 2017-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. | Guillaume Melquiond | 2015-10-13 |
| | |||
* | "allows to", like "allowing to", is improper | Jason Gross | 2014-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) | herbelin | 2010-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 11824 | herbelin | 2009-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 latex | notin | 2009-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: | herbelin | 2009-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'archive | herbelin | 2006-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 |