diff options
| author | Théo Zimmermann | 2019-07-04 13:17:13 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-07-04 13:17:13 +0200 |
| commit | 83a9451e4d6fd79ee7c529fb00c1d2e55bfbd6ad (patch) | |
| tree | f0985dd68e619f89c07ead8d805f7e912f4f6bf7 /doc/changelog/02-specification-language | |
| parent | 1c9aa339042030f756d1957abed7d3b698ff83f5 (diff) | |
Fix miscellaneous mistakes in unreleased changelog entries.
Diffstat (limited to 'doc/changelog/02-specification-language')
3 files changed, 7 insertions, 7 deletions
diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst index 79678c5242..279bb9272a 100644 --- a/doc/changelog/02-specification-language/10049-bidi-app.rst +++ b/doc/changelog/02-specification-language/10049-bidi-app.rst @@ -1,6 +1,6 @@ - New annotation in `Arguments` for bidirectionality hints: it is now possible to tell type inference to use type information from the context once the `n` first arguments of an application are known. The syntax is: - `Arguments foo x y & z`. - `#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with - help from Enrico Tassi + `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` + (`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with + help from Enrico Tassi). diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst index e3c3923348..2d17e569d3 100644 --- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst +++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst @@ -7,6 +7,6 @@ + notation :g:`(p | q)` now potentially clashes with core pattern syntax, and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. - see :ref:`extendedpatternmatching` for details + See :ref:`extendedpatternmatching` for details (`#10167 <https://github.com/coq/coq/pull/10167>`_, by Georges Gonthier). diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst index 21ec7f8e5b..71b10aaaf4 100644 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst @@ -1,11 +1,11 @@ -- Function always opens a proof when used with a ``measure`` or ``wf`` +- :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` annotation, see :ref:`advanced-recursive-functions` for the updated documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, by Enrico Tassi). -- The legacy command Add Morphism always opens a proof and cannot be used +- The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used inside a module type. In order to declare a module type parameter that - happens to be a morphism, use ``Parameter Morphism``. See + happens to be a morphism, use :cmd:`Declare Morphism`. See :ref:`deprecated_syntax_for_generalized_rewriting` for the updated documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, by Enrico Tassi). |