aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
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.
2018-09-12Manual: fix documentation of the “fresh” tacticVincent Laporte
2018-09-12Merge PR #8372: Grammar rule in the documentation of ssreflect's anonymous ↵Théo Zimmermann
arguments
2018-09-11building-a-coq-project-with-coq-makefile:fix typosJason Gross
make make-pretty-timed- after -> make make-pretty-timed-after (remove space between - and after) (and reflow paragraph) Fix spacing around :: in print-pretty-single-time-diff Closes #8396
2018-09-11Grammar entry for the ssr syntax for anonymous arguments.Assia Mahboubi
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10Documenting "Declare Scope".Hugo Herbelin
2018-09-10Merge PR #8104: Warnings on coercions used without being ImportedEnrico Tassi
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-09-07Recover lost snippetMatěj G
This snippet on pattern matching got lost in the process of migrating to Sphynx.
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
This warning makes it much easier to stop relying on `Set Automatic Coercions Import`. Tested with success on math-classes.
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-08-31Give a proper error message on num-not in functorJason Gross
Numeral Notations are not well-supported inside functors. We now give a proper error message rather than an anomaly when this occurs.
2018-08-31[numeral notations] support aliasesJason Gross
Aliases of global references can now be used in numeral notations
2018-08-31Add periods in response to PR commentsJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-12 00:09:57 +0000