aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
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-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-20Merge PR #9457: Correct W-Ind in Cic description of the reference manual.Théo Zimmermann
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-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-14Merge PR #9571: Document the now_show tactic.Clément Pit-Claudel
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
2019-02-12Fix failing coqtops in ltac.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coqide.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-specification-language.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in gallina-extensions.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in coq-library.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in cic.rstGaëtan Gilbert
2019-02-12Fix failing coqtops universe-polymorphism.rstGaëtan Gilbert
2019-02-12Improve the documentation of auto.Théo Zimmermann
2019-02-12Fix failing coqtops in ring.rstGaëtan Gilbert
2019-02-12Fix failing coqtops in micromega.rst (the main one requires csdp)Gaëtan Gilbert
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 04:27:39 +0000