aboutsummaryrefslogtreecommitdiff
path: root/Makefile.doc
AgeCommit message (Expand)Author
2020-07-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-20Omit volumnious Latex messagesJim Fehrle
2020-04-26Add sphinx_clean option to force full sphinx rebuildJim Fehrle
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-03-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-10Disable parallel build of Sphinx documentationMaxime Dénès
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-24Generate prodnCommands file that compares commands in the grammar toJim Fehrle
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-01-17[doc] [ltac2] Build Ltac2 documentation [make build system]Emilio Jesus Gallego Arias
2019-12-02Remove latex files that should be regenerated by makeJim Fehrle
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-06-17Update py-style headers to new year.Théo Zimmermann
2019-05-21Fixing typos - Part 1JPR
2019-05-05[make] build unreleased.rstEnrico Tassi
2019-04-27Amending CYGWIN fix in 63e7fb56923 so that it does not add a warning on MacOS.Hugo Herbelin
2019-03-26Fix make sphinx failureJim Fehrle
2019-03-05[make] Sphinx: install only `html/` and `latex/` directoriesVincent Laporte
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
2019-02-12Fix undefined SPHINX_DEPS when QUICKGaëtan Gilbert
2019-01-17Merge PR #9326: [ci] compile with -quick & validate after vio2voGaëtan Gilbert
2019-01-10[make] support for QUICKEnrico Tassi
2019-01-08Integrate plugin tutorial after code importGaëtan Gilbert
2018-10-10Include all menu entries in the menu/short TOC so that users can viewJim Fehrle
2018-10-02[doc] [api] Remove `ocamldoc` support in favor of `odoc`Emilio Jesus Gallego Arias
2018-09-25Fix Sphinx manual targets.Théo Zimmermann
2018-09-20Fix race condition.Théo Zimmermann
2018-09-20[doc] Add sphinx-html, sphinx-latex, and sphinx-pdf targetsClément Pit-Claudel
2018-09-03[doc] Build ML API documentation artifact.Emilio Jesus Gallego Arias
2018-08-29Create SPHINXWARNERROR variable that controls whether the SphinxJim Fehrle
2018-06-08gitlab: build sphinx doc in separate jobGaëtan Gilbert
2018-05-22[doc] Fix an incorrect use of $PWD in Makefile.docClément Pit-Claudel
2018-05-12Sphinx: a "QUICK=1" option to bypass recompilation of the library.Hugo Herbelin
2018-05-10Clean-up in Makefile.doc and include Sphinx in doc-html target.Théo Zimmermann
2018-05-10Remove tutorials.Théo Zimmermann
2018-04-28[doc] Remove unused dependencies.Emilio Jesus Gallego Arias
2018-04-16Remove LaTeX refman, now that migration to Sphinx is completeMaxime Dénès
2018-04-14[Sphinx] Build with warnings as errorsMaxime Dénès
2018-04-14[Sphinx] Move chapter 9 to new infrastructure.Théo Zimmermann
2018-04-13[Sphinx] Move chapter 1 to new infrastructureMaxime Dénès
2018-04-11[Sphinx] Move chapter 29 to new infrastructureMaxime Dénès
2018-04-10[Sphinx] Move chapter 6 to new infrastructureMaxime Dénès
2018-04-10[Sphinx] Move chapter 15 to new infrastructureMaxime Dénès
2018-04-09[Sphinx] Move chapter 7 to new infrastructureMaxime Dénès
2018-04-05[Sphinx] Move chapter 30 to new infrastructureMaxime Dénès
2018-04-04[Sphinx] Move chapter 28 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Move chapter 27 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Move chapter 25 to new infrastructureMaxime Dénès