aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-10-28 10:03:17 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-10-28 17:08:56 +0100
commit0a1b046d37761fe47435d5041bb5031e3f7d6613 (patch)
tree943f3fdbeade3cb065dcfc09d343062e505485a9
parent110f7b41eca9c3e22fff0df67419b57d9c2ef612 (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.ml3
-rw-r--r--library/lib.mli1
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 *)