aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/02-specification-language
diff options
context:
space:
mode:
authorJim Fehrle2021-03-07 10:15:11 -0800
committerJim Fehrle2021-03-30 09:51:56 -0700
commiteeb142f3c69d2467fbadd7dd1470ac1606b2e5bf (patch)
tree6057d6c11961f6398fcca77313b0e8abcaaa8961 /doc/changelog/02-specification-language
parent16d9e9cf378b9eb0ee0fc42c5c0a3a23b3df6ff4 (diff)
Remove the :> type cast
Diffstat (limited to 'doc/changelog/02-specification-language')
-rw-r--r--doc/changelog/02-specification-language/13911-master.rst4
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/13911-master.rst b/doc/changelog/02-specification-language/13911-master.rst
new file mode 100644
index 0000000000..a0b37dd2d9
--- /dev/null
+++ b/doc/changelog/02-specification-language/13911-master.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+ The little used `:>` type cast, which was only interpreted in Program-mode
+ (`#13911 <https://github.com/coq/coq/pull/13911>`_,
+ by Jim Fehrle and Théo Zimmermann).