aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2019-03-25[Vernacular] Deprecate the “Show Script” commandVincent Laporte
Fixes #8320
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
This option made the Coercions command follow non-standard scoping rules (effect on `Require` rather than `Import`). It was already marked for deletion in 8.8.
2019-03-25Fix indentationGan Shen
2019-03-25Update doc/sphinx/language/gallina-extensions.rstThéo Zimmermann
Co-Authored-By: gshen42 <gan.shen@outlook.com>
2019-03-24Fix typoGan Shen
2019-03-22Merge PR #8560: Unicode bindings for CoqIDE that works out of the boxPierre-Marie Pédrot
Reviewed-by: Zimmi48 Ack-by: charguer Reviewed-by: gares Reviewed-by: ppedrot
2019-03-21Merge PR #9789: [Manual] Improve documentation on Section, Variable, ContextThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: jfehrle
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jfehrle
2019-03-18[Manual] Parametrize -> ParametErizeLysxia
- Refine some `@term` into `@type`
2019-03-18Update doc and changesKazuhiko Sakaguchi
2019-03-18[Manual] Move command Context after Let, and more polishingLysxia
- Refine some `@term` into `@type`
2019-03-18fix documentation issues, and add entry to change logcharguer
2019-03-18polishing documentation for coqide bindings, following @Zimmi48 commentscharguer
2019-03-18final polishing for coqide bindingscharguer
2019-03-18documentation for unicode bindingscharguer
2019-03-17[Manual] Move doc on Let into Section mechanism, and more polishingLysxia
- Put "Section mechanism" example earlier
2019-03-17[Manual] Gather section-specific commands in Section documentation (fix #9704)Lysxia
2019-03-17[Manual] Improve chapter Type classes, and add mention of Context under VariableLysxia
- More consistent code indentation - Nest command variants properly - Make `Context` explanation a bit less terse, with more links - Typesetting bits, add some :cmd: links
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Add StrictProp.v with basic SProp related definitionsGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
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-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-28Merge PR #9578: Document primitive integersThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-02-26[dune] Simple rule to generate Stdlib's documentation.Emilio Jesus Gallego Arias
Ideally this will be handled by Dune's native library support, but this could be useful for the likes of #9648. I am not sure what should be done w.r.t. style files.
2019-02-26Merge PR #9567: [vernac] Unify declaration hooks.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: mattam82 Reviewed-by: maximedenes
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
Supersedes #8718.
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
Reviewed-by: SkySkimmer
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 23:29:16 +0000