diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-28 10:03:17 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-28 17:08:56 +0100 |
| commit | 0a1b046d37761fe47435d5041bb5031e3f7d6613 (patch) | |
| tree | 943f3fdbeade3cb065dcfc09d343062e505485a9 /library/libobject.ml | |
| parent | 110f7b41eca9c3e22fff0df67419b57d9c2ef612 (diff) | |
lib_stack: API to reorder the libstack
For discharging it is important that constants occur in the libstack
in an order that respects the dependencies among them. This is
impossible to achieve for private constants when they are exported globally
without this (ugly IMO) api.
Diffstat (limited to 'library/libobject.ml')
0 files changed, 0 insertions, 0 deletions