aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2018-03-15[Sphinx] Move chapter 16 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 14Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
2018-03-15[Sphinx] Move chapter 14 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 13Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
2018-03-15[Sphinx] Move chapter 13 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 12Maxime Dénès
Thanks to Clément Pit-Claudel for porting this chapter.
2018-03-15[Sphinx] Move chapter 12 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 10Maxime Dénès
Thanks to Calvin Beck for porting this chapter.
2018-03-15[Sphinx] Move chapter 10 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 8Maxime Dénès
Thanks to Heiko Becker and Nikita Zyuzin for porting this chapter.
2018-03-15[Sphinx] Move chapter 8 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 5Maxime Dénès
Thanks to Richard Ford for porting this chapter.
2018-03-15[Sphinx] Move chapter 5 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 4Maxime Dénès
Thanks to Richard Ford for porting this chapter.
2018-03-15[Sphinx] Move chapter 4 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 2Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
2018-03-15[Sphinx] Move chapter 2 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add creditsMaxime Dénès
2018-03-15[Sphinx] Move credits to new infrastructureMaxime Dénès
2018-03-13[Sphinx] Add introductionMaxime Dénès
I backported changes done to the LaTeX manual.
2018-03-13[Sphinx] Move introduction to new infrastructureMaxime Dénès
2018-03-13[Sphinx] Add "edit on github"Maxime Dénès
2018-03-13[Sphinx] Mention licenseMaxime Dénès
2018-03-13[Sphinx] Remove ad-hoc color for links interfering with TOCMaxime Dénès
2018-03-13[Sphinx] Update some metadataMaxime Dénès
2018-03-13[Sphinx] Read version number from configureMaxime Dénès
2018-03-13[Sphinx] Comment out metadata for unused backendsMaxime Dénès
2018-03-13[Sphinx] Remove information for .chm backendMaxime Dénès
2018-03-13[Sphinx] add bibliographyMaxime Dénès
2018-03-13[Sphinx] Add indexesMaxime Dénès
2018-03-12[Sphinx] Add table of contentsMaxime Dénès
2018-03-12[Sphinx] Add doc preambleMaxime Dénès
2018-03-12[Sphinx] Add a few grammar constructionsMaxime Dénès
Code from Paul Steckler (MIT).
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Documentation for Cumulativity Weak Constraints.Gaëtan Gilbert
2018-03-09Merge PR #6480: Allow Prop as source for coercionsMaxime Dénès
2018-03-09Merge PR #6818: Sphinx doc infrastructureMaxime Dénès
2018-03-09Moving Gitlab CI documentation build to the main Coq build.Maxime Dénès
2018-03-09Integration of a sphinx-based documentation generator.Maxime Dénès
The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content.
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-09doc and changes for coercion from prop/typecharguer
2018-03-09Merge PR #6937: Add empty compat file for Coq 8.8Maxime Dénès
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
Following up on #6791, we remove support refolding in reduction. We also update a test case that was not properly understood, see the discussion in #6895.
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-08Merge PR #6903: [compat] Remove "Shrink Abstract"Maxime Dénès
2018-03-07Add empty compat file for Coq 8.8Jason Gross
This closes #6598
2018-03-06Remove outdated information regarding the FAQ.Théo Zimmermann
The FAQ is not part of the Coq sources anymore.
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
Following up on #6791, we the option "Shrink Abstract".
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 16:38:12 +0000