diff options
| author | Emilio Jesus Gallego Arias | 2019-06-25 03:19:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:36:08 +0200 |
| commit | 20254d7fa38c99608042a878ec0c2975f9887ce6 (patch) | |
| tree | d8dff9da05b146815484022ac736e69a51841e8b /kernel/nativecode.ml | |
| parent | 5f3118f6caf5f6fe2942c61ab5146bf725483937 (diff) | |
[declare] Remove superfluous API
`declare_definition` didn't improve a lot the declare path and was
used only once on interesting code. Also, it had many optional
parameters. The declare path is critical enough as to care about a
tidy API.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions