From 0a1b046d37761fe47435d5041bb5031e3f7d6613 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 10:03:17 +0100 Subject: 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. --- library/lib.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'library/lib.ml') 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)) -- cgit v1.2.3