| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-13 | [dune] [doc] Support for building the reference manual with Dune. | Emilio Jesus Gallego Arias | |
| This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted. | |||
| 2018-10-15 | Correct some spelling errors | Benjamin 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-01 | Merge PR #8301: Documentation for proof diffs | Théo Zimmermann | |
| 2018-09-25 | [doc] Fix GH-8529: wrap macro definitions in math delimiters for MathJax | Clément Pit-Claudel | |
| 2018-09-23 | Update flag, option and table descriptions in coqdomain.py, update ↵ | Jim Fehrle | |
| README.rst to match. Bump env_version. | |||
| 2018-09-23 | Documentation for proof diffs | Jim Fehrle | |
| 2018-09-20 | Define 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 directive | Clé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/4979 | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Ensure that merging coqtop blocks preserves anchors | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Work around https://github.com/sphinx-doc/sphinx/issues/4980 | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix a typo in the developer guide | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Add env_version to metadata of coqrst plugin | Clé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 build | Clé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 file | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix a typo in coqdomain.py | Clément Pit-Claudel | |
| 2018-08-31 | Merge PR #8170: Don't index names starting with `_` in docs | Théo Zimmermann | |
| 2018-08-22 | Fix #8251: remove "the the" occurrences | Gaëtan Gilbert | |
| 2018-07-30 | [sphinx] Use arguments of '.. example::' directive as a title | Clé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_signature | Clément Pit-Claudel | |
| 2018-07-25 | [sphinx] Add a way of skipping names in the indexes. | Théo Zimmermann | |
| 2018-06-21 | Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵ | Maxime Dénès | |
| understands. | |||
| 2018-06-20 | On cygwin, pass the filename in a format that coqdoc understands. | Jim Fehrle | |
| 2018-06-19 | [doc] Rewrite and document the prodn directive | Clé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-08 | gitlab: build sphinx doc in separate job | Gaëtan Gilbert | |
| 2018-05-25 | [doc] Allow more than one signature and name per Sphinx object | Clément Pit-Claudel | |
| As discussed in GH-7556. | |||
| 2018-05-25 | Merge PR #7556: Add a setting to warn about empty object in the refman | Maxime Dénès | |
| 2018-05-22 | [doc] Add a setting to warn about empty Coq objects | Clément Pit-Claudel | |
| 2018-05-16 | [sphinx] Bump timeout. Closes #7532. | Clément Pit-Claudel | |
| 2018-05-15 | [doc] More feedback on doc writer guide | Clément Pit-Claudel | |
| Co-Authored-By: @Zimmi48 | |||
| 2018-05-15 | [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 | |
| 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 domain | Clé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 time | Clément Pit-Claudel | |
| 2018-05-09 | [sphinx] Warn for dangling tacn / cmd / opt / ... references. | Clément Pit-Claudel | |
| 2018-04-16 | Merge PR #7251: doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing | Maxime Dénès | |
| 2018-04-14 | [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 | |
| 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 grammars | Maxime Dénès | |
| 2018-03-16 | [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-12 | [Sphinx] Add a few grammar constructions | Maxime Dénès | |
| Code from Paul Steckler (MIT). | |||
| 2018-03-09 | 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 | |
| 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-13 | Fix some typos. | Guillaume Melquiond | |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason 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-19 | Hopefully 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |