diff options
| author | Tej Chajed | 2018-07-26 10:02:45 -0400 |
|---|---|---|
| committer | Tej Chajed | 2018-07-26 10:04:33 -0400 |
| commit | afbf03722cae08f610d53e02efb68b6ea6f35cc2 (patch) | |
| tree | 80887aeb13f56a4a7d02d6bb40c644c3e2343d51 /kernel/nativevalues.ml | |
| parent | 85d5f45d7a5374646a31f8829965bbfed0a95070 (diff) | |
Add information to option type errors
Print the expected and actual types for the option value (which is one
of bool, int, or string).
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions