diff options
| author | Armaël Guéneau | 2018-06-21 14:22:35 +0200 |
|---|---|---|
| committer | Armaël Guéneau | 2018-06-25 17:53:09 +0200 |
| commit | 9795f080f4536586aac8108a49217a6c58957e5b (patch) | |
| tree | 1452644114ac29b262e7d887929f003ca734e619 /kernel/nativecode.ml | |
| parent | 24279abf43cfbd65e2fc29f171eb8705fdf61a3e (diff) | |
Clarify the message "this hint will only be used by eauto"
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions