aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-14 22:24:23 +0200
committerHugo Herbelin2020-04-14 22:24:23 +0200
commite75ad2a575bc73febbf7eb075545e95d102f7544 (patch)
treed713a28697b993574c57408f66eb15b457ac46ad /doc
parente56ac87a12db577ec5f9b6ab521245e9a60f4812 (diff)
parent74d733a11cd942847a24fedca9cbc0583190162d (diff)
Merge PR #11957: [stdlib] update sigma-type notations
Reviewed-by: JasonGross Ack-by: herbelin
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/10-standard-library/11957-signotations.rst4
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/11957-signotations.rst b/doc/changelog/10-standard-library/11957-signotations.rst
new file mode 100644
index 0000000000..fc5d434274
--- /dev/null
+++ b/doc/changelog/10-standard-library/11957-signotations.rst
@@ -0,0 +1,4 @@
+- **Added:**
+ notations for sigma types: ``{ x & P & Q }``, ``{ ' pat & P }``, ``{ ' pat & P & Q }``
+ (`#11957 <https://github.com/coq/coq/pull/11957>`_,
+ by Olivier Laurent).