aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2018-10-01Merge PR #8301: Documentation for proof diffsThéo Zimmermann
2018-09-28Small fixes in attribute documentation.Théo Zimmermann
In particular, move the footnotes back to the foot of the chapter.
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-26Merge PR #8504: Allow successive attributes #[foo] #[bar]Vincent Laporte
2018-09-26Merge PR #8419: Remove romega in favor of liaThéo Zimmermann
2018-09-26Allow successive attributes #[foo] #[bar]Gaëtan Gilbert
2018-09-26Combined Scheme tests sort to use either "*" or "/\"Théo Winterhalter
And update documentation.
2018-09-25Fix title of Introduction chapter in HTML version.Théo Zimmermann
And location of footnote.
2018-09-25[doc] Rename credits-wrapper to credits and credits to credits-contentsClément Pit-Claudel
This ensures that previous links to 'credits.html' still point to the right page.
2018-09-25[doc] Change Sphinx project title back to "Coq"Clément Pit-Claudel
Use 'The Coq Reference Manual' only in LaTeX.
2018-09-25[doc] Fix GH-8529: wrap macro definitions in math delimiters for MathJaxClément Pit-Claudel
2018-09-25Remove romegaVincent Laporte
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-21Universe binders are Id, not Name. Never print Var.Gaëtan Gilbert
Comes with minor cleanups in exception catching and unnecessary mapi.
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag:
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] Replace app.info (deprecated in Sphinx 8.0) with logger.infoClément Pit-Claudel
2018-09-20[doc] Remove unneeded backslashes in biblio.bibClément Pit-Claudel
2018-09-20[doc] Skip unneeded copies in copy_formatspecific_filesClément Pit-Claudel
2018-09-20[doc] Move a citation back into the introductionClément Pit-Claudel
Alternatively, we could duplicate the citation text in both index files.
2018-09-20[doc] Remove frames around code snippets in the LateX buildClément Pit-Claudel
2018-09-20[doc] Change the name that appears on the first page of the PDF manualClément Pit-Claudel
2018-09-20[doc] Fix some Sphinx LaTeX warnings and silence othersClément Pit-Claudel
2018-09-20[doc] Add another common mistake to the documentation-writing guideClément Pit-Claudel
2018-09-20[doc] Fix a few syntax highlighting issuesClément Pit-Claudel
2018-09-20[doc] Get rid of two Sphinx warningsClément Pit-Claudel
2018-09-20[doc] Fix more duplicate-label issues in production listsClément Pit-Claudel
2018-09-20[doc] Add more common mistakes to the documentation-writing guideClément Pit-Claudel
2018-09-20[doc] Mark the dummy index files as orphans (the LaTeX build skips them)Clément Pit-Claudel
Do we really need these? Wouldn't it be better to just add appropriate links to the html template?
2018-09-20[doc] Add a warning about overusing the `coqtop` directiveClément Pit-Claudel
2018-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979Clément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Improve rendering of Coq objects in PDF outputClément Pit-Claudel
2018-09-20[doc] Fix a few LaTeX mistakesClément Pit-Claudel
2018-09-20[doc] Create a wrapper around the Credits file for the LaTeX buildClément Pit-Claudel
2018-09-20[doc] Create a separate zebibliography file for the LaTeX buildClément Pit-Claudel
`.. bibliography::` puts the bibliography on its own page with its own title in LaTeX, but includes it inline without a title in HTML [1], so we need to maintain two separate copies of zebibliography.rst [1] https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends
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] Remove an empty '.. bibliography::' in addendum/programClément Pit-Claudel
2018-09-20[doc] Explain why zebibliography needs to be separate and oddly-namedClément Pit-Claudel
2018-09-20[doc] Adjust conf.py to allow LaTeX buildsClément Pit-Claudel
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-09-19Merge PR #7343: Add missing index entries.Maxime Dénès
2018-09-17Add missing index entries.Théo Zimmermann
In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249.
2018-09-16Mising prime in the subtyping rulesJoachim Breitner
2018-09-16Missing space in cic.rstJoachim Breitner
2018-09-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-13Add doc for template polymorphism option and attributes.Gaëtan Gilbert
2018-09-12Remove quote pluginMaxime Dénès
As far as I know, this plugin is untested and barely maintained. I don't think it has real use cases any more, so let's move it out from the repo and see if somebody wants to take over and maintain it. We also remove the documentation, which was telling our users to look at ring to see an example of reification done using quote, when in fact it wasn't using it anymore.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 05:30:24 +0000