Merge PR #11404: replace RList by list R in all files where it is used in this directory

Ack-by: SkySkimmer
Reviewed-by: herbelin

1 files changed, 15 insertions, 0 deletions

diff --git a/doc/changelog/10-standard-library/11404-removeRList.rst b/doc/changelog/10-standard-library/11404-removeRList.rst
new file mode 100644
index 0000000000..88e22d128c
--- /dev/null
+++ b/doc/changelog/10-standard-library/11404-removeRList.rst
@@ -0,0 +1,15 @@
+- **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).