aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-20Define flags (binary-valued settings) and tables (settings that are sets)Jim Fehrle
2018-09-20Update minimum required dependency versions of Sphinx doc.Théo Zimmermann
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
2018-09-20[doc] Add sphinx-html, sphinx-latex, and sphinx-pdf targetsClément Pit-Claudel
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] Rewrite and document the prodn directiveClé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
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] Ensure that merging coqtop blocks preserves anchorsClément Pit-Claudel
2018-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4980Clément Pit-Claudel
2018-09-20[doc] Fix a typo in the developer guideClé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] Add env_version to metadata of coqrst pluginClé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
2018-09-20[doc] Create a separate index file for the LaTeX buildClément Pit-Claudel
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
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
2018-09-12Manual: fix documentation of the “fresh” tacticVincent Laporte
2018-09-12Merge PR #8372: Grammar rule in the documentation of ssreflect's anonymous ar...Théo Zimmermann
2018-09-11building-a-coq-project-with-coq-makefile:fix typosJason Gross
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