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/lib.mli | |
| 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/lib.mli')
| -rw-r--r-- | library/lib.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/lib.mli b/library/lib.mli index b67b2b873..bb8831759 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -55,6 +55,7 @@ val segment_of_objects : val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.obj -> unit +val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) |