diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/13415-intern-univs.rst | 5 | ||||
| -rw-r--r-- | doc/changelog/06-ssreflect/13473-test_pred.rst | 4 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 |
3 files changed, 10 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/13415-intern-univs.rst b/doc/changelog/03-notations/13415-intern-univs.rst new file mode 100644 index 0000000000..e9f51461e5 --- /dev/null +++ b/doc/changelog/03-notations/13415-intern-univs.rst @@ -0,0 +1,5 @@ +- **Fixed:** Notations understand universe names without getting + confused by different imported modules between declaration and use + locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes + `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan + Gilbert). diff --git a/doc/changelog/06-ssreflect/13473-test_pred.rst b/doc/changelog/06-ssreflect/13473-test_pred.rst new file mode 100644 index 0000000000..3c7df11540 --- /dev/null +++ b/doc/changelog/06-ssreflect/13473-test_pred.rst @@ -0,0 +1,4 @@ +- **Added:** + Adding a test that the notations `{in _, _}` and `{pred _}` from `ssrbool.v` are displayed correctly. + (`#13473 <https://github.com/coq/coq/pull/13473>`_, + by Cyril Cohen). diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7201dc6a0e..8ab4265b15 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -709,6 +709,7 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq811.v theories/Compat/Coq812.v theories/Compat/Coq813.v + theories/Compat/Coq814.v </dd> <dt> <b>Array</b>: |