diff options
Diffstat (limited to 'doc')
5 files changed, 32 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/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). |