diff options
| author | Pierre-Marie Pédrot | 2019-05-21 19:00:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | 2fa3dc389a58ca4a390b99995d82e6c089add163 (patch) | |
| tree | 32ec7005bbbee5acfef94679fd4d475fc647e068 /doc/plugin_tutorial/tuto1/src | |
| parent | b245a6c46bc3ef70142e8a165f6cde54265b941e (diff) | |
Move body_of_constant_body to Global and specialize its uses.
This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.
The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src')
0 files changed, 0 insertions, 0 deletions