aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-03-07Merge PR #9133: Move README-V1-V5 to credits chapterClément Pit-Claudel
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-03-01[doc] ssr: Fix the documentation of `by [tacs]`Erik Martin-Dorel
2019-02-28Add DOIs.Théo Zimmermann
2019-02-28Move content of README-V1-V5 to Credits chapter.Théo Zimmermann
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
2019-02-28Merge PR #9578: Document primitive integersThéo Zimmermann
2019-02-26[dune] Simple rule to generate Stdlib's documentation.Emilio Jesus Gallego Arias
2019-02-26Merge PR #9567: [vernac] Unify declaration hooks.Maxime Dénès
2019-02-25[Manual] Refactor documentation of internal registration commandsVincent Laporte
2019-02-25[Manual] Document primitive integersVincent Laporte
2019-02-25[Manual] Document the “Primitive” commandVincent Laporte
2019-02-25[Manual] Document “Register Inline”Vincent Laporte
2019-02-25[Manual] Document “Register” to kernel namespaceVincent Laporte
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-02-21Stdlib HTML documentation: fix a few absolute URLsVincent Laporte
2019-02-20Merge PR #9457: Correct W-Ind in Cic description of the reference manual.Théo Zimmermann
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
2019-02-19Merge PR #9501: Sphinx: fail when a command fails + other stuffClément Pit-Claudel
2019-02-19[sphinx] Refactor handling of options for coqtop directive.Théo Zimmermann
2019-02-19Make the conclusion of local contexts W-Ind empty.Tanaka Akira
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-18[sphinx] Add abort and restart options to directive coqtop.Théo Zimmermann
2019-02-18coqdomain.py fix typo in commentGaëtan Gilbert
2019-02-18Sphinx: nicer error reportingGaëtan Gilbert
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
2019-02-18Fix doc for Refine Instance ModeGaëtan Gilbert
2019-02-18Sphinx: remove [coqtop:: undo]Gaëtan Gilbert
2019-02-18Fix last nested lemma failure.Théo Zimmermann
2019-02-18Fix failing coqtops in type-classes.rstGaëtan Gilbert
2019-02-18Merge PR #9568: Add test that we regenerated doc/sphinx/README.rst to linterThéo Zimmermann
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-18Add diff rule for README.rst to dune refman-html aliasGaëtan Gilbert
2019-02-17Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.Pierre-Marie Pédrot
2019-02-14Merge PR #9571: Document the now_show tactic.Clément Pit-Claudel
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
2019-02-14Document the now_show tactic.Théo Zimmermann
2019-02-14[Manual] Fix a referenceVincent Laporte
2019-02-14[Manual] Clean examples for `apply`Vincent Laporte
2019-02-14[Manual] Don’t use `Undo` in ssreflect examplesVincent Laporte
2019-02-14[Manual] Clean examples about `inversion` tacticVincent Laporte
2019-02-13Merge PR #9450: Fix #9432: canonical structure and coercion accept universe b...Maxime Dénès
2019-02-13[ssr] move shorter Canonical to Coq properEnrico Tassi
2019-02-13Merge PR #9564: Fix small errors in cic.rst (3rd)Théo Zimmermann
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
2019-02-12Fix failing coqtops in syntax-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in tactics.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in ssreflect-proof-language.rstGaëtan Gilbert