aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-13[refman] Fix Sphinx-translation regression in Arguments command.Théo Zimmermann
2019-03-13[refman] Remove warning silencing by fixing the underlying issue.Théo Zimmermann
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-03-12[refman] Add 'warn' option to coqtop directive.Théo Zimmermann
Fix semantic conflict between #9389 and #9654.
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jashug
2019-03-10Merge PR #9654: [sphinx] Add warn option to coqtop directive.Clément Pit-Claudel
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: vbgl Reviewed-by: cpitclaudel
2019-03-08[sphinx] Fix typo in local application of tacticshawnzug
2019-03-07Merge PR #9133: Move README-V1-V5 to credits chapterClément Pit-Claudel
Reviewed-by: cpitclaudel
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 22:34:16 +0000