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/06-ssreflect | |
| 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/06-ssreflect')
| -rw-r--r-- | doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst | 3 | ||||
| -rw-r--r-- | doc/changelog/06-ssreflect/10932-void-type-ssr.rst | 3 | ||||
| -rw-r--r-- | doc/changelog/06-ssreflect/11136-inj_compr.rst | 2 |
3 files changed, 5 insertions, 3 deletions
diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst index 5e005742fd..424540b46a 100644 --- a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst +++ b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst @@ -1,4 +1,5 @@ -- Generalize tactics :tacn:`under` and :tacn:`over` for any registered +- **Added:** + Generalize tactics :tacn:`under` and :tacn:`over` for any registered relation. More precisely, assume the given context lemma has type `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The first step performed by :tacn:`under` (since Coq 8.10) amounts to diff --git a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst index 7366ef1190..1dbb3035ce 100644 --- a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst +++ b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst @@ -1,3 +1,4 @@ -- Add a :g:`void` notation for the standard library empty type (:g:`Empty_set`) +- **Added:** + A :g:`void` notation for the standard library empty type (:g:`Empty_set`) (`#10932 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de Amorim). diff --git a/doc/changelog/06-ssreflect/11136-inj_compr.rst b/doc/changelog/06-ssreflect/11136-inj_compr.rst index b546fcde6b..7ebf95b988 100644 --- a/doc/changelog/06-ssreflect/11136-inj_compr.rst +++ b/doc/changelog/06-ssreflect/11136-inj_compr.rst @@ -1,2 +1,2 @@ -- Added lemma :g:`inj_compr` to :g:`ssr.ssrfun` +- **Added:** Lemma :g:`inj_compr` to :g:`ssr.ssrfun` (`#11136 <https://github.com/coq/coq/pull/11136>`_, by Cyril Cohen). |