diff options
Diffstat (limited to 'library/libobject.mli')
| -rw-r--r-- | library/libobject.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/library/libobject.mli b/library/libobject.mli index 15de388ea..33ad67c84 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -51,6 +51,14 @@ open Mod_subst this function should be declared for substitutive objects only (see obove) + * a discharge function, that is applied at section closing time to + collect the data necessary to rebuild the discharged form of the + non volatile objects + + * a rebuild function, that is applied after section closing to + rebuild the non volatile content of a section from the data + collected by the discharge function + * an export function, to enable optional writing of its contents to disk (.vo). This function is also the oportunity to remove redundant information in order to keep .vo size small |