diff options
Diffstat (limited to 'doc/changelog')
11 files changed, 59 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst b/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst new file mode 100644 index 0000000000..fc909e7a1d --- /dev/null +++ b/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst @@ -0,0 +1,8 @@ +- **Fixed:** + Issues in the presence of notations recursively referring to another + applicative notations, such as missing scope propagation, or failure + to use a notation for printing + (`#12960 <https://github.com/coq/coq/pull/12960>`_, + fixes `#9403 <https://github.com/coq/coq/issues/9403>`_ + and `#10803 <https://github.com/coq/coq/issues/10803>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12979-doc-numbers.rst b/doc/changelog/03-notations/12979-doc-numbers.rst new file mode 100644 index 0000000000..631bd6ec69 --- /dev/null +++ b/doc/changelog/03-notations/12979-doc-numbers.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + :n:`Numeral Notation`, please use :ref:`Number Notation <number-notations>` instead. + (`#12979 <https://github.com/coq/coq/pull/12979>`_, + by Pierre Roux). diff --git a/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst b/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst new file mode 100644 index 0000000000..42b62eed75 --- /dev/null +++ b/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst @@ -0,0 +1,7 @@ +- **Fixed:** + Fixing printing of notations in custom entries with + variables not mentioning an explicit level + (`#13026 <https://github.com/coq/coq/pull/13026>`_, + fixes `#12775 <https://github.com/coq/coq/issues/12775>`_ + and `#13018 <https://github.com/coq/coq/issues/13018>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst b/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst new file mode 100644 index 0000000000..50aa4a9052 --- /dev/null +++ b/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Repairing option :g:`Display parentheses` in CoqIDE + (`#12794 <https://github.com/coq/coq/pull/12794>`_ and `#13067 <https://github.com/coq/coq/pull/13067>`_, + fixes `#12793 <https://github.com/coq/coq/issues/12793>`_, + by Jean-Christophe Léchenet and Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst b/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst new file mode 100644 index 0000000000..b444a2f436 --- /dev/null +++ b/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst @@ -0,0 +1,6 @@ +- **Added:** + :tacn:`replace` and :tacn:`inversion` support registration of a + :g:`core.identity`-like equality in :g:`Type`, such as HoTT's :g:`path` + (`#12847 <https://github.com/coq/coq/pull/12847>`_, + partially fixes `#12846 <https://github.com/coq/coq/issues/12846>`_, + by Hugo Herbelin). diff --git a/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst b/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst new file mode 100644 index 0000000000..a191716b2f --- /dev/null +++ b/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst @@ -0,0 +1,6 @@ +- **Fixed:** + printing of the quotation qualifiers when printing :g:`Ltac` functions + (`#13028 <https://github.com/coq/coq/pull/13028>`_, + fixes `#9716 <https://github.com/coq/coq/issues/9716>`_ + and `#13004 <https://github.com/coq/coq/issues/13004>`_, + by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst b/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst new file mode 100644 index 0000000000..c67b0f6e80 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst @@ -0,0 +1,4 @@ +- **Removed:** + In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. + Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 <https://github.com/coq/coq/pull/6261>`_ + (`#13016 <https://github.com/coq/coq/pull/13016>`_, by Jim Fehrle). diff --git a/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst b/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst new file mode 100644 index 0000000000..75b1e26248 --- /dev/null +++ b/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Targets such as ``print-pretty-timed`` in ``coq_makefile``-made + ``Makefile``\s no longer error in rare cases where ``--output-sync`` is not + passed to make and the timing output gets interleaved in just the wrong way + (`#13063 <https://github.com/coq/coq/pull/13063>`_, fixes `#13062 + <https://github.com/coq/coq/issues/13062>`_, by Jason Gross). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst b/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst new file mode 100644 index 0000000000..855aa360f1 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst @@ -0,0 +1,4 @@ +- **Added:** + Coq is now tested against OCaml 4.11.1 + (`#12972 <https://github.com/coq/coq/pull/12972>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst new file mode 100644 index 0000000000..c142eec561 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst @@ -0,0 +1,4 @@ +- **Removed:** + The `num` library is not linked to Coq anymore + (`#13007 <https://github.com/coq/coq/pull/13007>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst b/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst new file mode 100644 index 0000000000..d17a2dff6b --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst @@ -0,0 +1,5 @@ +- **Fixed:** + The reference manual can now build with Sphinx 3 + (`#13011 <https://github.com/coq/coq/pull/13011>`_, + fixes `#12332 <https://github.com/coq/coq/issues/12332>`_, + by Théo Zimmermann and Jim Fehrle). |