aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2018-10-13Merge PR #8652: Add missing indexes for Hint Cut and Hint Mode.Clément Pit-Claudel
2018-10-11Documenting -arg in _CoqProject.Hugo Herbelin
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-10Merge PR #8384: Small fixes in attribute documentation.Clément Pit-Claudel
2018-10-10[doc] [sphinx] Fix title levels.Théo Zimmermann
2018-10-10Include all menu entries in the menu/short TOC so that users can viewJim Fehrle
2018-10-10Fix names for 2 entries in Flags, Options, Tables index.Jim Fehrle
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
2018-10-05Rename CHANGES to CHANGES.md.Guillaume Melquiond
2018-10-04Add missing indexes for Hint Cut and Hint Mode.Théo Zimmermann
2018-10-03Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the com...Théo Zimmermann
2018-10-02Update the -compat flagsJason Gross
2018-10-02[doc] Nits on utilities / toplevel building.Emilio Jesus Gallego Arias
2018-10-01Docs: Missing backquoteJoachim Breitner
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
2018-10-01Merge PR #8301: Documentation for proof diffsThéo Zimmermann
2018-09-28Small fixes in attribute documentation.Théo Zimmermann
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
2018-09-25Fix Sphinx manual targets.Théo Zimmermann
2018-09-25Fix title of Introduction chapter in HTML version.Théo Zimmermann
2018-09-25[doc] Rename credits-wrapper to credits and credits to credits-contentsClément Pit-Claudel
2018-09-25[doc] Change Sphinx project title back to "Coq"Clément Pit-Claudel
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 README.rst...Jim Fehrle
2018-09-23Documentation for proof diffsJim Fehrle
2018-09-21Universe binders are Id, not Name. Never print Var.Gaëtan Gilbert
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