aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/changes.rst
AgeCommit message (Collapse)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
2021-02-22mention --version to CoqIDEEnrico Tassi
2021-02-22changelog for 8.13.1Enrico Tassi
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-01-21Improve wording for #13384Jim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-04Changelog for 8.13.0Enrico Tassi
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-11[changes] mark #12765 as experimentalEnrico Tassi
2020-12-10Changelog for 8.12.2.Théo Zimmermann
2020-12-06[doc] update changes after 13501Enrico Tassi
2020-12-03Implement review corrections by Théo ZimmermannMatthieu Sozeau
2020-12-03Implement suggestions by Théo ZimmermannMatthieu Sozeau
2020-12-03Apply suggestions from code reviewMatthieu Sozeau
Co-authored-by: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-12-03Apply suggestions from code reviewEnrico Tassi
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Update doc/sphinx/changes.rstMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Fixes in the summary by Jim FehrleMatthieu Sozeau
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-12-03Changes without PR references fixesMatthieu Sozeau
2020-12-03Apply suggestions from @jfehrle code reviewMatthieu Sozeau
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-11-24Convert auto chapter to prodnJim Fehrle
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:45:57 +0000