aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 5995a9600..94cba5e0c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -95,6 +95,10 @@ let add_anonymous_entry node =
add_entry sp node;
sp
+let add_absolutely_named_lead sp obj =
+ cache_object (sp,obj);
+ add_entry sp (Leaf obj)
+
let add_leaf id kind obj =
let sp = make_path id kind in
cache_object (sp,obj);