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.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/lib.ml')
| -rw-r--r-- | library/lib.ml | 3 |
1 files changed, 3 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)) |