aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Expand)Author
2018-12-11Add missing formatting.Théo Zimmermann
2018-12-11Document the deprecation of hint declaration withou database in refman.Théo Zimmermann
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-06Improve rendering of the credits.Guillaume Melquiond
2018-10-24[Manual] Prevent an irrelevant warning to show upVincent Laporte
2018-10-24[Manual] Avoid using deprecated “Focus”Vincent Laporte
2018-10-24[Manual] Fix rendering of an exampleVincent Laporte
2018-10-24[Manual] TypoVincent Laporte
2018-10-24[Manual] Fix an exampleVincent Laporte
2018-10-24[Manual] Fix layout of a listVincent Laporte
2018-10-23Fix formatting. Use standard if..then grammar.Sam Pablo Kuper
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-13Merge PR #8616: Include the full Table of Contents document in the on-screen ...Clément Pit-Claudel
2018-10-13Merge PR #8652: Add missing indexes for Hint Cut and Hint Mode.Clément Pit-Claudel
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-04Add missing indexes for Hint Cut and Hint Mode.Théo Zimmermann
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-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-26Combined Scheme tests sort to use either "*" or "/\"Théo Winterhalter
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-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979Clément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-17Add missing index entries.Théo Zimmermann
2018-09-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-12Remove quote pluginMaxime Dénès
2018-09-12Manual: fix documentation of the “fresh” tacticVincent Laporte
2018-09-11Grammar entry for the ssr syntax for anonymous arguments.Assia Mahboubi
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-08-29Merge PR #8353: [sphinx] Fix timeout issue by splitting imports.Clément Pit-Claudel
2018-08-29Merge PR #8345: Add index for focusing braces.Clément Pit-Claudel
2018-08-29[sphinx] Fix timeout issue by splitting imports.Théo Zimmermann
2018-08-28Merge PR #8135: Sphinx fixing of the beginning of the Tactics chapter.Clément Pit-Claudel
2018-08-28Add index for focusing braces.Théo Zimmermann
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-24Merge PR #8266: Minor Sphinx improvements in the bullet documentation.Clément Pit-Claudel
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-22Add missing spaces.Théo Zimmermann
2018-08-22[sphinx] Improve Case analysis and induction section.Théo Zimmermann