diff options
| author | Yves Bertot | 2020-01-16 13:28:28 +0100 |
|---|---|---|
| committer | Yves Bertot | 2020-02-06 17:53:31 +0100 |
| commit | 0fe99a0d6a4d643cf311200c870aeaff042d7069 (patch) | |
| tree | 4140ca1e18e3918385c263ca31db2dae8fff1ef3 /doc | |
| parent | c6e89e2b13d7fa99aaaaf02fc3430ae6c5f00beb (diff) | |
replace RList by list R
add an overlay for coquelicot
remove functions from RList: In, Rlength, cons_Rlist, app_RList
because they are essentially the same as In, length, app, and map from List
(beware that the order of arguments changes for map, and the In function
contains reversed equalities).
adds deprecation warnings for Rlist and Rlength
adds deprecated notations for RList.cons and RList.nil
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/11404-removeRList.rst | 15 |
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). |