diff options
| author | Pierre-Marie Pédrot | 2018-11-03 19:41:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-03 19:41:11 +0100 |
| commit | 782736024e75a67c7dd1cbb7801b217f72f79fe5 (patch) | |
| tree | 9ab84e41d80db908a1b1efb1ec8ed541ba5f6505 /kernel/nativelib.ml | |
| parent | 2e970d6c7876963a9845cae4153fe39cac81b587 (diff) | |
| parent | baa8812294d48bf9d0e6e62a39440e9ffb2b93e2 (diff) | |
Merge PR #8877: Fix #8876: expected number of arguments for cumulative constructors
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions