aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)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
Closes coq/coq#9669
2019-02-28Add DOIs.Théo Zimmermann
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
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
This is intended to be separate from handling of implicit binders. The remaining uses of declare_manual_implicits satisfy a lot of assertions, giving the possibility of simplifying the interface in the future. Two disabled warnings are added for things that currently pass silently. Currently only Mtac passes non-maximal implicits to declare_manual_implicits with the force-usage flag set. When implicit arguments don't have to be named, should move Mtac over to set_implicits.
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
By default Coq warnings are made fatal when building the manual. If you want to show a command resulting in a warning, use the warn option. Preexisting warnings are either fixed or marked as expected.
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
Reviewed-by: SkySkimmer
2019-02-19Merge PR #9501: Sphinx: fail when a command fails + other stuffClément Pit-Claudel
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel Reviewed-by: ejgallego
2019-02-19[sphinx] Refactor handling of options for coqtop directive.Théo Zimmermann
Make it mandatory to give exactly one display option.
2019-02-19Make the conclusion of local contexts W-Ind empty.Tanaka Akira
The conclusion of W-Ind, "\WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ}", is changed to "\WF{E;~\ind{p}{Γ_I}{Γ_C}}{}" because local contexts should be empty when inductive definition is defined globally. This is consistent with W-Global-Assum and W-Global-Def. The side condition "c_i ∉ Γ ∪ E" which I changed previous commit is changed again to "c_i ∉ E" because I guess that it tries to avoid name conflicts to the local contexts in the conclusion. However, the condition is useless after the local contexts is empty.
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: ppedrot
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
This uses a new coqtop-only option "Coqtop Exit On Error", not sure where to put the doc for it. It being an option means we can locally turn it off (.. coqtop:: fail).
2019-02-18Fix doc for Refine Instance ModeGaëtan Gilbert
2019-02-18Sphinx: remove [coqtop:: undo]Gaëtan Gilbert
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
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
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2019-02-18Add diff rule for README.rst to dune refman-html aliasGaëtan Gilbert
We change regen_readme such that when given an argument it outputs there instead of overwriting the readme. Prompted by me noticing I forgot to regen in #9553.
2019-02-14Merge PR #9571: Document the now_show tactic.Clément Pit-Claudel
Ack-by: Zimmi48 Reviewed-by: cpitclaudel
2019-02-14Document the now_show tactic.Théo Zimmermann
It was used in the standard library and the test-suite but undocumented so far.
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 ↵Maxime Dénès
binders. Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Reviewed-by: maximedenes
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
Reviewed-by: Zimmi48
2019-02-13Merge PR #9553: Sphinx various fixing of failing commandsThéo Zimmermann
Ack-by: Zimmi48
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
Mostly in the pattern ~~~ .. coqtop:: in Theorem foo : bla. Theorem bar : blah. (* nested proof error *) ~~~
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
In particular, mention that auto does not use full-blown apply.
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
Maybe we should still let it run but let's disable it until we install csdp on the build server at least.
2019-02-12Fix failing coqtops in generalized-rewriting.rstGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 11:50:32 +0000