From d0f2961b1e4c4f8153d1deb3ea7a3e5fc1eb22cc Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 13 May 2019 15:36:43 +0200 Subject: Move last changelog entries for 8.10+beta1. --- .../03-notations/10061-print-custom-grammar.rst | 4 -- doc/changelog/04-tactics/09996-hint-mode.rst | 5 --- doc/changelog/04-tactics/10059-change-no-check.rst | 7 --- doc/changelog/06-ssreflect/09995-notations.rst | 8 ---- .../09984-pairusualdecidabletypefull.rst | 3 -- doc/changelog/12-misc/09964-changes.rst | 14 ------ doc/sphinx/changes.rst | 50 +++++++++++++++++++++- 7 files changed, 49 insertions(+), 42 deletions(-) delete mode 100644 doc/changelog/03-notations/10061-print-custom-grammar.rst delete mode 100644 doc/changelog/04-tactics/09996-hint-mode.rst delete mode 100644 doc/changelog/04-tactics/10059-change-no-check.rst delete mode 100644 doc/changelog/06-ssreflect/09995-notations.rst delete mode 100644 doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst delete mode 100644 doc/changelog/12-misc/09964-changes.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/10061-print-custom-grammar.rst b/doc/changelog/03-notations/10061-print-custom-grammar.rst deleted file mode 100644 index 8786c7ce6b..0000000000 --- a/doc/changelog/03-notations/10061-print-custom-grammar.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` - (`#10061 `_, - fixes `#9681 `_, - by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst deleted file mode 100644 index 06e9059b45..0000000000 --- a/doc/changelog/04-tactics/09996-hint-mode.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Modes are now taken into account by :tacn:`typeclasses eauto` for - local hypotheses - (`#9996 `_, - fixes `#5752 `_, - by Maxime Dénès, review by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst deleted file mode 100644 index 987b2a8ccd..0000000000 --- a/doc/changelog/04-tactics/10059-change-no-check.rst +++ /dev/null @@ -1,7 +0,0 @@ -- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a - documented replacement of :tacn:`convert_concl_no_check` - (`#10012 `_, - `#10017 `_, - `#10053 `_, and - `#10059 `_, - by Hugo Herbelin and Paolo G. Giarrusso). diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst deleted file mode 100644 index 3dfc45242d..0000000000 --- a/doc/changelog/06-ssreflect/09995-notations.rst +++ /dev/null @@ -1,8 +0,0 @@ -- `inE` now expands `y \in r x` when `r` is a `simpl_rel`. - New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion - class, simplified `predType` interface: `pred_class` and `mkPredType` - deprecated, `{pred T}` and `PredType` should be used instead. - `if c return t then ...` now expects `c` to be a variable bound in `t`. - New `nonPropType` interface matching types that do _not_ have sort `Prop`. - New `relpre R f` definition for the preimage of a relation R under f - (`#9995 `_, by Georges Gonthier). diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst deleted file mode 100644 index 732c088f45..0000000000 --- a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` - (`#9984 `_, - by Jean-Christophe Léchenet and Oliver Nash). diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst deleted file mode 100644 index dd873cfdd5..0000000000 --- a/doc/changelog/12-misc/09964-changes.rst +++ /dev/null @@ -1,14 +0,0 @@ -- Changelog has been moved from a specific file `CHANGES.md` to the - reference manual; former Credits chapter of the reference manual has - been split in two parts: a History chapter which was enriched with - additional historical information about Coq versions 1 to 5, and a - Changes chapter which was enriched with the content formerly in - `CHANGES.md` and `COMPATIBILITY` - (`#9133 `_, - `#9668 `_, - `#9939 `_, - `#9964 `_, - and `#10085 `_, - by Théo Zimmermann, - with help and ideas from Emilio Jesús Gallego Arias, Gaëtan - Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 574b943a78..be22071f66 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -355,6 +355,11 @@ Other changes in 8.10+beta1 that will do it automatically, using the output of ``coqc`` (`#8638 `_, by Jason Gross). + - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` + (`#10061 `_, + fixes `#9681 `_, + by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). + - The `quote plugin `_ was removed. If some users are interested in maintaining this plugin @@ -400,7 +405,23 @@ Other changes in 8.10+beta1 closes `#7632 `_, by Théo Zimmermann). - - SSReflect clear discipline made consistent across the entire proof language. + - Modes are now taken into account by :tacn:`typeclasses eauto` for + local hypotheses + (`#9996 `_, + fixes `#5752 `_, + by Maxime Dénès, review by Pierre-Marie Pédrot). + + - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a + documented replacement of :tacn:`convert_concl_no_check` + (`#10012 `_, + `#10017 `_, + `#10053 `_, and + `#10059 `_, + by Hugo Herbelin and Paolo G. Giarrusso). + +- SSReflect: + + - Clear discipline made consistent across the entire proof language. Whenever a clear switch `{x..}` comes immediately before an existing proof context entry (used as a view, as a rewrite rule or as name for a new context entry) then such entry is cleared too. @@ -414,6 +435,15 @@ Other changes in 8.10+beta1 (`#9341 `_, by Enrico Tassi). + - `inE` now expands `y \in r x` when `r` is a `simpl_rel`. + New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion + class, simplified `predType` interface: `pred_class` and `mkPredType` + deprecated, `{pred T}` and `PredType` should be used instead. + `if c return t then ...` now expects `c` to be a variable bound in `t`. + New `nonPropType` interface matching types that do _not_ have sort `Prop`. + New `relpre R f` definition for the preimage of a relation R under f + (`#9995 `_, by Georges Gonthier). + - Vernacular commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. @@ -535,10 +565,28 @@ Other changes in 8.10+beta1 `fset` database (`#9725 `_, by Frédéric Besson). + - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` + (`#9984 `_, + by Jean-Christophe Léchenet and Oliver Nash). + - Some error messages that show problems with a pair of non-matching values will now highlight the differences (`#8669 `_, by Jim Fehrle). +- Changelog has been moved from a specific file `CHANGES.md` to the + reference manual; former Credits chapter of the reference manual has + been split in two parts: a History chapter which was enriched with + additional historical information about Coq versions 1 to 5, and a + Changes chapter which was enriched with the content formerly in + `CHANGES.md` and `COMPATIBILITY` + (`#9133 `_, + `#9668 `_, + `#9939 `_, + `#9964 `_, + and `#10085 `_, + by Théo Zimmermann, + with help and ideas from Emilio Jesús Gallego Arias, Gaëtan + Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). Version 8.9 ----------- -- cgit v1.2.3 From 5a172d9afaddf44e702af66f80bd5649031c9e4a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 13 May 2019 16:38:40 +0200 Subject: Missing change entry for #9854. --- doc/sphinx/changes.rst | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index be22071f66..cca3b2e06b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -419,6 +419,15 @@ Other changes in 8.10+beta1 `#10059 `_, by Hugo Herbelin and Paolo G. Giarrusso). + - The simplified value returned by :tacn:`field_simplify` is not + always a fraction anymore. When the denominator is :g:`1`, it + returns :g:`x` while previously it was returning :g:`x/1`. This + change could break codes that were post-processing application of + :tacn:`field_simplify` to get rid of these :g:`x/1` + (`#9854 `_, + by Laurent Théry, + with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte). + - SSReflect: - Clear discipline made consistent across the entire proof language. -- cgit v1.2.3