Richard W.M. Jones
250ee85839
Rework Std_utils.Option so it works like the OCaml stdlib module
...
OCaml 4.08 introduces a stdlib Option module which looks a bit like
ours but has a number of differences. In particular our functions
Option.may and Option.default have no corresponding functions in
stdlib, although there are close enough equivalents.
This change was automated using this command:
$ perl -pi.bak \
-e 's/Option.may/Option.iter/g; s/Option.default /Option.value ~default:/g' \
`git ls-files`
Update common module to include:
commit cffa077323fafcdfcf78e230c022afa891a6b3ff
Author: Richard W.M. Jones <rjones@redhat.com >
Date: Mon Feb 20 12:11:51 2023 +0000
mlstdutils: Rework the Option module to be compatible with stdlib
2023-02-20 12:14:08 +00:00
..
2022-03-09 09:28:02 +00:00
2019-05-30 09:12:32 +02:00
2017-07-27 17:31:41 +01:00
2022-08-16 10:39:01 +01:00
2017-07-27 22:31:22 +01:00
2023-02-20 12:14:08 +00:00
2017-07-27 17:31:41 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-07-10 17:01:59 +01:00
2023-02-07 10:50:48 +00:00
2017-07-27 17:31:41 +01:00
2022-06-17 13:24:19 +01:00
2022-08-16 10:39:01 +01:00
2016-07-26 10:43:45 +01:00
2022-08-16 10:39:01 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2018-02-06 17:27:23 +01:00
2018-02-06 17:27:23 +01:00
2023-02-07 10:50:48 +00:00
2021-03-16 11:24:37 +00:00
2017-09-16 22:27:16 +01:00
2018-01-09 12:17:53 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-08-08 17:50:23 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-07-27 17:31:41 +01:00
2017-07-27 17:31:41 +01:00
2017-07-27 17:31:41 +01:00
2023-02-07 10:50:48 +00:00
2017-07-10 17:01:59 +01:00
2023-02-07 10:50:48 +00:00
2018-04-19 11:30:29 +02:00
2016-07-26 10:43:45 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2016-07-26 10:43:45 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-07-27 17:31:41 +01:00
2017-07-27 17:31:41 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-09-16 22:27:16 +01:00
2022-08-16 10:39:01 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-20 12:14:08 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-20 12:14:08 +00:00
2017-07-27 17:31:41 +01:00
2018-02-12 11:24:06 +01:00
2023-02-07 10:50:48 +00:00
2021-05-13 12:04:41 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-07-27 17:31:41 +01:00
2021-09-07 14:53:06 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-01-19 23:00:23 +00:00
2021-11-09 10:20:37 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-03-03 11:32:37 +00:00
2017-07-27 17:31:41 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-08-08 17:50:23 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2022-05-03 10:54:00 +02:00
2023-02-07 10:50:48 +00:00
2022-05-26 10:16:21 +01:00
2023-02-07 10:50:48 +00:00
2017-07-27 17:31:41 +01:00
2017-07-27 17:31:41 +01:00
2022-05-11 17:02:17 +02:00
2020-07-30 13:58:35 +01:00
2017-07-27 17:31:41 +01:00
2017-07-27 17:31:41 +01:00
2017-07-27 17:31:41 +01:00
2017-07-27 17:31:41 +01:00
2017-07-10 17:01:59 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2017-07-27 17:31:41 +01:00
2023-02-07 10:50:48 +00:00
2017-07-27 17:31:41 +01:00
2017-07-27 22:31:22 +01:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2018-05-15 11:15:54 +01:00
2023-02-07 10:50:48 +00:00
2021-11-09 10:20:37 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2023-02-07 10:50:48 +00:00
2021-03-30 12:56:58 +01:00
2021-10-12 16:48:04 +02:00
2023-02-07 10:50:48 +00:00
2017-07-27 17:31:41 +01:00