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 /kernel/nativecode.ml | |
| 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 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions