aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2018-03-15[Sphinx] Move chapter 16 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 14Maxime Dénès
2018-03-15[Sphinx] Move chapter 14 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 13Maxime Dénès
2018-03-15[Sphinx] Move chapter 13 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 12Maxime Dénès
2018-03-15[Sphinx] Move chapter 12 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 10Maxime Dénès
2018-03-15[Sphinx] Move chapter 10 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 8Maxime Dénès
2018-03-15[Sphinx] Move chapter 8 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 5Maxime Dénès
2018-03-15[Sphinx] Move chapter 5 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 4Maxime Dénès
2018-03-15[Sphinx] Move chapter 4 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 2Maxime Dénès
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
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
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
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
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
2018-03-06Remove outdated information regarding the FAQ.Théo Zimmermann
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias