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 | |
| 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.
| -rw-r--r-- | library/lib.ml | 3 | ||||
| -rw-r--r-- | library/lib.mli | 1 |
2 files changed, 4 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index cdc888903..297441e6e 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -198,6 +198,9 @@ let split_lib_at_opening sp = let add_entry sp node = lib_stk := (sp,node) :: !lib_stk +let pull_to_head oname = + lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk + let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) 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 *) |