diff options
Diffstat (limited to 'doc/changelog/10-standard-library/11404-removeRList.rst')
| -rw-r--r-- | doc/changelog/10-standard-library/11404-removeRList.rst | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/doc/changelog/10-standard-library/11404-removeRList.rst b/doc/changelog/10-standard-library/11404-removeRList.rst deleted file mode 100644 index 88e22d128c..0000000000 --- a/doc/changelog/10-standard-library/11404-removeRList.rst +++ /dev/null @@ -1,15 +0,0 @@ -- **Removed:** - Type `RList` has been removed. All uses have been replaced by `list R`. - Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist` - have also been removed as they are essentially the same as `In`, `length`, - `app`, and `map` from `List`, modulo the following changes: - - - `RList.In x (RList.cons a l)` used to be convertible to - `(x = a) \\/ RList.In x l`, - but `List.In x (a :: l)` is convertible to - `(a = x) \\/ List.In l`. - The equality is reversed. - - `app_Rlist` and `List.map` take arguments in different order. - - (`#11404 <https://github.com/coq/coq/pull/11404>`_, - by Yves Bertot). |