aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/changes.rst
AgeCommit message (Collapse)Author
2020-11-19Fix typo in rst link syntax.Théo Zimmermann
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog.
2020-11-12Move last changelog entry for 8.12.1.Théo Zimmermann
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-10-23Correct doc using :>>Gaëtan Gilbert
The cast keywords are <: and <<:, not :>/:>> :>> stopped being a keyword in #13106
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Ack-by: ppedrot
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-17Wording improvements.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-07-13Advertise switch to maintainer teams and credit maintainers.Théo Zimmermann
2020-06-26Credit Erik Martin-Dorel for work on Docker.Théo Zimmermann
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
2020-06-09Summary of changes for 8.12Matthieu Sozeau
Includes fixes to changes by Jim, Enrico and Théo Fix local links, for 8.12 and 8.11
2020-06-06Merge PR #12380: Fix #12361 (indexing issues in the PDF)Théo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
2020-06-05Merge PR #12460: Add remaining 8.12+beta1 changelog entries.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
2020-06-05Document incompatibility with Sphinx 3.Théo Zimmermann
Cf. #12332
2020-06-05[sphinx] Get rid of anonymous targets (Sphinx 2.3.1 doesn't like them)Clément Pit-Claudel
https://github.com/sphinx-doc/sphinx/issues/7701
2020-05-27Add more changelog entries which have been backported to v8.12.Théo Zimmermann
2020-05-27[changelog/8.12] Wording improvements.Théo Zimmermann
2020-05-27[changelog/8.12] Use sections and provide a local TOC.Théo Zimmermann
2020-05-27[changelog/8.12] Split misc entries out in more relevant sections.Théo Zimmermann
2020-05-27Changelog entries for the 8.12 changes to the reference manual.Théo Zimmermann
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-24Fix hyperlinks in changes.rstMatthew Dempsky
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
Reviewed-by: vbgl
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-23Merge PR #12117: Make multiplication of Cauchy reals transparent and ↵Hugo Herbelin
accelerate it Reviewed-by: herbelin
2020-04-22Document Cauchy realsVincent Semeria
2020-04-20[refman] Remove references to omega from Tactics chapter.Théo Zimmermann
Omega was defined twice and this is the tactics chapter documentation which was refered to from the tactic index. We remove it so that users find the other reference (which contains the deprecation notice). The changes to the doc of zarith are a follow-up to #11976.
2020-04-03Adding changelog for 8.11.1.Pierre-Marie Pédrot
2020-03-28Document change of behavior of Fail in 8.11.Théo Zimmermann
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-24Merge PR #11892: [refman] Fix caching, which was broken by the addition of ↵Théo Zimmermann
coq_config Reviewed-by: Zimmi48
2020-03-23[refman] Fix caching, which was broken by the addition of coq_configClément Pit-Claudel
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
2020-03-19Adapt to sub-TOC not showing in PDF output.Théo Zimmermann
2020-01-23More minor tweaks to the 8.11 changelog.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-01-23Add missing 'and'.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-01-22Minor tweaks to the 8.11 changelog.Théo Zimmermann
2020-01-22Insert changelog entry for #11430 from v8.11 branch.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 05:11:30 +0000