diff options
| author | Théo Zimmermann | 2019-10-22 11:20:07 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-28 10:04:32 +0100 |
| commit | fbdde37d9d7d2fce7fe9b7035ad0e8efa7799dff (patch) | |
| tree | a6d68fd1a86a6e6adbae7d6dcf0e76f09425efe5 /doc/changelog/05-tactic-language | |
| parent | 570018fe2c37eee1f87d509037162768bffe6366 (diff) | |
[changelog] Add types to changelog entries.
Types of changes are defined in the list defined by Keep a Changelog
1.0.0 (https://keepachangelog.com/en/1.0.0/):
- Added
- Changed
- Deprecated
- Fixed
- Removed
We exclude the type Security for now, even for soundness fixes,
because the process of handling security vulnerabilities is different
from anything we follow right now.
Diffstat (limited to 'doc/changelog/05-tactic-language')
3 files changed, 6 insertions, 3 deletions
diff --git a/doc/changelog/05-tactic-language/10002-ltac2.rst b/doc/changelog/05-tactic-language/10002-ltac2.rst index 6d62f11eff..8b910a4779 100644 --- a/doc/changelog/05-tactic-language/10002-ltac2.rst +++ b/doc/changelog/05-tactic-language/10002-ltac2.rst @@ -1,4 +1,5 @@ -- Ltac2, a new version of the tactic language Ltac, that doesn't +- **Added:** + Ltac2, a new version of the tactic language Ltac, that doesn't preserve backward compatibility, has been integrated in the main Coq distribution. It is still experimental, but we already recommend users of advanced Ltac to start using it and report bugs or request diff --git a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst index bd1c0c42e8..f32443cbb9 100644 --- a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst +++ b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst @@ -1,4 +1,5 @@ -- Ltac2 tactic notations with “constr” arguments can specify the +- **Added:** + Ltac2 tactic notations with “constr” arguments can specify the interpretation scope for these arguments; see :ref:`ltac2_notations` for details (`#10289 <https://github.com/coq/coq/pull/10289>`_, diff --git a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst index fba09f5e87..16ca9caf48 100644 --- a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst +++ b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst @@ -1,4 +1,5 @@ -- White spaces are forbidden in the “&ident” syntax for ltac2 references +- **Changed:** + White spaces are forbidden in the :n:`&@ident` syntax for ltac2 references that are described in :ref:`ltac2_built-in-quotations` (`#10324 <https://github.com/coq/coq/pull/10324>`_, fixes `#10088 <https://github.com/coq/coq/issues/10088>`_, |