diff options
| author | Pierre-Marie Pédrot | 2020-05-09 15:56:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-14 12:38:08 +0200 |
| commit | 5e1da5b05860750606f32063a221d6023cabf5dc (patch) | |
| tree | fdc2927a9ad56a7745b22e33610af8aee3442518 /kernel/nativevalues.ml | |
| parent | 2e53445be16ef28058599fed3f06424db17f6943 (diff) | |
Tweak the error message of reference internalization.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions