diff options
| author |  jadep <jade.philipoom@gmail.com> | 2019-04-03 14:45:32 -0400 |
|---|---|---|
| committer | jadephilipoom <jade.philipoom@gmail.com> | 2019-04-03 23:34:53 +0100 |
| commit | bd34d676010ebf6dd4aa5076537f89572803dd3d (patch) | |
| tree | bbc634fa51d071a4bd1e55019dc6853ecd936622 /src/Language.v | |
| parent | ee30e8faf778ac9fd43f1d8d9d6d61cd4e9d8b3f (diff) | |
partition -> Partition.partition to prevent confusion with List.partition
Diffstat (limited to 'src/Language.v')
0 files changed, 0 insertions, 0 deletions