From 81301b55df9c52fe5503421eb9527bb04a1643e0 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 30 Apr 2019 11:42:23 +0200 Subject: Create categories in changelog. --- .gitattributes | 1 + doc/changelog/00-title.rst | 2 ++ doc/changelog/00000-title.rst | 2 -- doc/changelog/01-kernel/00000-title.rst | 3 +++ doc/changelog/02-specification-language/00000-title.rst | 3 +++ doc/changelog/03-notations/00000-title.rst | 3 +++ doc/changelog/04-tactics/00000-title.rst | 3 +++ doc/changelog/04-tactics/09996-hint-mode.rst | 5 +++++ doc/changelog/04-tactics/10059-change-no-check.rst | 7 +++++++ doc/changelog/05-tactic-language/00000-title.rst | 3 +++ doc/changelog/06-ssreflect/00000-title.rst | 3 +++ doc/changelog/06-ssreflect/09995-notations.rst | 8 ++++++++ doc/changelog/07-commands-and-options/00000-title.rst | 3 +++ doc/changelog/08-tools/00000-title.rst | 3 +++ doc/changelog/09-coqide/00000-title.rst | 3 +++ doc/changelog/09984-pairusualdecidabletypefull.rst | 3 --- doc/changelog/09995-notations.rst | 8 -------- doc/changelog/09996-hint-mode.rst | 5 ----- doc/changelog/10-standard-library/00000-title.rst | 3 +++ .../10-standard-library/09984-pairusualdecidabletypefull.rst | 3 +++ doc/changelog/10059-change-no-check.rst | 7 ------- doc/changelog/11-infrastructure-and-dependencies/00000-title.rst | 3 +++ doc/changelog/12-misc/00000-title.rst | 3 +++ doc/changelog/README.md | 7 ++++--- doc/dune | 2 +- 25 files changed, 67 insertions(+), 29 deletions(-) create mode 100644 doc/changelog/00-title.rst delete mode 100644 doc/changelog/00000-title.rst create mode 100644 doc/changelog/01-kernel/00000-title.rst create mode 100644 doc/changelog/02-specification-language/00000-title.rst create mode 100644 doc/changelog/03-notations/00000-title.rst create mode 100644 doc/changelog/04-tactics/00000-title.rst create mode 100644 doc/changelog/04-tactics/09996-hint-mode.rst create mode 100644 doc/changelog/04-tactics/10059-change-no-check.rst create mode 100644 doc/changelog/05-tactic-language/00000-title.rst create mode 100644 doc/changelog/06-ssreflect/00000-title.rst create mode 100644 doc/changelog/06-ssreflect/09995-notations.rst create mode 100644 doc/changelog/07-commands-and-options/00000-title.rst create mode 100644 doc/changelog/08-tools/00000-title.rst create mode 100644 doc/changelog/09-coqide/00000-title.rst delete mode 100644 doc/changelog/09984-pairusualdecidabletypefull.rst delete mode 100644 doc/changelog/09995-notations.rst delete mode 100644 doc/changelog/09996-hint-mode.rst create mode 100644 doc/changelog/10-standard-library/00000-title.rst create mode 100644 doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst delete mode 100644 doc/changelog/10059-change-no-check.rst create mode 100644 doc/changelog/11-infrastructure-and-dependencies/00000-title.rst create mode 100644 doc/changelog/12-misc/00000-title.rst diff --git a/.gitattributes b/.gitattributes index 58b1a31d36..260e3f96b6 100644 --- a/.gitattributes +++ b/.gitattributes @@ -54,6 +54,7 @@ dune* whitespace=blank-at-eol,tab-in-indent .gitattributes whitespace=blank-at-eol,tab-in-indent _CoqProject whitespace=blank-at-eol,tab-in-indent Dockerfile whitespace=blank-at-eol,tab-in-indent +00000-title.rst -whitespace # tabs are allowed in Makefiles. Makefile* whitespace=blank-at-eol diff --git a/doc/changelog/00-title.rst b/doc/changelog/00-title.rst new file mode 100644 index 0000000000..628d9c8578 --- /dev/null +++ b/doc/changelog/00-title.rst @@ -0,0 +1,2 @@ +Unreleased changes +------------------ diff --git a/doc/changelog/00000-title.rst b/doc/changelog/00000-title.rst deleted file mode 100644 index 628d9c8578..0000000000 --- a/doc/changelog/00000-title.rst +++ /dev/null @@ -1,2 +0,0 @@ -Unreleased changes ------------------- diff --git a/doc/changelog/01-kernel/00000-title.rst b/doc/changelog/01-kernel/00000-title.rst new file mode 100644 index 0000000000..f680628a05 --- /dev/null +++ b/doc/changelog/01-kernel/00000-title.rst @@ -0,0 +1,3 @@ + +**Kernel** + diff --git a/doc/changelog/02-specification-language/00000-title.rst b/doc/changelog/02-specification-language/00000-title.rst new file mode 100644 index 0000000000..99bd2c5b44 --- /dev/null +++ b/doc/changelog/02-specification-language/00000-title.rst @@ -0,0 +1,3 @@ + +**Specification language, type inference** + diff --git a/doc/changelog/03-notations/00000-title.rst b/doc/changelog/03-notations/00000-title.rst new file mode 100644 index 0000000000..abc532df11 --- /dev/null +++ b/doc/changelog/03-notations/00000-title.rst @@ -0,0 +1,3 @@ + +**Notations** + diff --git a/doc/changelog/04-tactics/00000-title.rst b/doc/changelog/04-tactics/00000-title.rst new file mode 100644 index 0000000000..3c7802d632 --- /dev/null +++ b/doc/changelog/04-tactics/00000-title.rst @@ -0,0 +1,3 @@ + +**Tactics** + diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst new file mode 100644 index 0000000000..06e9059b45 --- /dev/null +++ b/doc/changelog/04-tactics/09996-hint-mode.rst @@ -0,0 +1,5 @@ +- 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 new file mode 100644 index 0000000000..987b2a8ccd --- /dev/null +++ b/doc/changelog/04-tactics/10059-change-no-check.rst @@ -0,0 +1,7 @@ +- 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/05-tactic-language/00000-title.rst b/doc/changelog/05-tactic-language/00000-title.rst new file mode 100644 index 0000000000..b34d190298 --- /dev/null +++ b/doc/changelog/05-tactic-language/00000-title.rst @@ -0,0 +1,3 @@ + +**Tactic language** + diff --git a/doc/changelog/06-ssreflect/00000-title.rst b/doc/changelog/06-ssreflect/00000-title.rst new file mode 100644 index 0000000000..2e724627ec --- /dev/null +++ b/doc/changelog/06-ssreflect/00000-title.rst @@ -0,0 +1,3 @@ + +**SSReflect** + diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst new file mode 100644 index 0000000000..3dfc45242d --- /dev/null +++ b/doc/changelog/06-ssreflect/09995-notations.rst @@ -0,0 +1,8 @@ +- `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/07-commands-and-options/00000-title.rst b/doc/changelog/07-commands-and-options/00000-title.rst new file mode 100644 index 0000000000..1a0272983e --- /dev/null +++ b/doc/changelog/07-commands-and-options/00000-title.rst @@ -0,0 +1,3 @@ + +**Commands and options** + diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst new file mode 100644 index 0000000000..bf462744fb --- /dev/null +++ b/doc/changelog/08-tools/00000-title.rst @@ -0,0 +1,3 @@ + +**Tools** + diff --git a/doc/changelog/09-coqide/00000-title.rst b/doc/changelog/09-coqide/00000-title.rst new file mode 100644 index 0000000000..0fc27cf380 --- /dev/null +++ b/doc/changelog/09-coqide/00000-title.rst @@ -0,0 +1,3 @@ + +**CoqIDE** + diff --git a/doc/changelog/09984-pairusualdecidabletypefull.rst b/doc/changelog/09984-pairusualdecidabletypefull.rst deleted file mode 100644 index 732c088f45..0000000000 --- a/doc/changelog/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/09995-notations.rst b/doc/changelog/09995-notations.rst deleted file mode 100644 index 3dfc45242d..0000000000 --- a/doc/changelog/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/09996-hint-mode.rst b/doc/changelog/09996-hint-mode.rst deleted file mode 100644 index 06e9059b45..0000000000 --- a/doc/changelog/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/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst new file mode 100644 index 0000000000..d517a0e709 --- /dev/null +++ b/doc/changelog/10-standard-library/00000-title.rst @@ -0,0 +1,3 @@ + +**Standard library** + diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst new file mode 100644 index 0000000000..732c088f45 --- /dev/null +++ b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst @@ -0,0 +1,3 @@ +- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` + (`#9984 `_, + by Jean-Christophe Léchenet and Oliver Nash). diff --git a/doc/changelog/10059-change-no-check.rst b/doc/changelog/10059-change-no-check.rst deleted file mode 100644 index 987b2a8ccd..0000000000 --- a/doc/changelog/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/11-infrastructure-and-dependencies/00000-title.rst b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst new file mode 100644 index 0000000000..6b301f59d3 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst @@ -0,0 +1,3 @@ + +**Infrastructure and dependencies** + diff --git a/doc/changelog/12-misc/00000-title.rst b/doc/changelog/12-misc/00000-title.rst new file mode 100644 index 0000000000..5e709e2b27 --- /dev/null +++ b/doc/changelog/12-misc/00000-title.rst @@ -0,0 +1,3 @@ + +**Miscellaneous** + diff --git a/doc/changelog/README.md b/doc/changelog/README.md index 64359e45ba..2891eb207e 100644 --- a/doc/changelog/README.md +++ b/doc/changelog/README.md @@ -14,9 +14,10 @@ entry in [`dev/doc/changes.md`](../../dev/doc/changes.md). ## How to add an entry? ## -You should create a file in this folder. The name of the file should -be `NNNNN-identifier.rst` where `NNNNN` is the number of the pull -request on five digits and `identifier` is whatever you want. +You should create a file in one of the sub-directories. The name of +the file should be `NNNNN-identifier.rst` where `NNNNN` is the number +of the pull request on five digits and `identifier` is whatever you +want. This file should use the same format as the reference manual (as it will be copied in there). You may reference the documentation you just diff --git a/doc/dune b/doc/dune index 06f78013aa..3a8efbb36d 100644 --- a/doc/dune +++ b/doc/dune @@ -23,7 +23,7 @@ (rule (targets unreleased.rst) (deps (source_tree changelog)) - (action (with-stdout-to %{targets} (bash "cat changelog/*.rst")))) + (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) ; The install target still needs more work. ; (install -- cgit v1.2.3