aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-09-21Removing calls to AUContext.instance.Pierre-Marie Pédrot
2018-09-21Fix printing of abstract universe contexts.Pierre-Marie Pédrot
2018-09-21Merge commit 6a8c37c02504463afaa677641d75d9977020edf6 Windows buildfile clean...Michael Soegtrop
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-21[dune] [configure] Allow to set prefix using environment variable.Emilio Jesus Gallego Arias
2018-09-21Merge PR #8518: [dune] Add "watch" target for continuous build mode.Théo Zimmermann
2018-09-20[dune] Add "watch" target for continuous build mode.Emilio Jesus Gallego Arias
2018-09-20Define flags (binary-valued settings) and tables (settings that are sets)Jim Fehrle
2018-09-20CHANGES for 8.8.2.Théo Zimmermann
2018-09-20Current diff code only compares the first current goal of the old and newJim Fehrle
2018-09-20Use "rm -rf" so .coq-native directories are removed. Fixes #8496.Jim Fehrle
2018-09-20[opam] Fix typo in build variable.Emilio Jesus Gallego Arias
2018-09-20Merge PR #8418: Add a PDF version of the manualThéo Zimmermann
2018-09-20Merge PR #8297: Fix #7754: universe declarations on mutual inductivesMatthieu Sozeau
2018-09-20Stop building LaTeX doc in Travis (keep HTML).Théo Zimmermann
2018-09-20Mention PDF doc in CHANGES.Théo Zimmermann
2018-09-20Fix race condition.Théo Zimmermann
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