portage Astterm (partiellement)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@159 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 3 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 07d4049ce7..46a2833f57 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -26,6 +26,8 @@ type library_entry = section_path * node
 
 let lib_stk = ref ([] : (section_path * node) list)
 
+let lib_tab = Hashtbl.create 353
+
 let module_name = ref None
 let path_prefix = ref ([] : string list)
 
@@ -69,7 +71,8 @@ let split_lib sp =
 (* Adding operations. *)
 
 let add_entry sp node =
-  lib_stk := (sp,node) :: !lib_stk
+  lib_stk := (sp,node) :: !lib_stk;
+  Hashtbl.add lib_tab sp node
 
 let anonymous_id = 
   let n = ref 0 in
@@ -77,7 +80,8 @@ let anonymous_id =
 
 let add_anonymous_entry node =
   let sp = make_path (anonymous_id()) OBJ in
-  add_entry sp node
+  add_entry sp node;
+  sp
 
 let add_leaf id kind obj =
   let sp = make_path id kind in
@@ -88,12 +92,16 @@ let add_anonymous_leaf obj =
   add_anonymous_entry (Leaf obj)
 
 let add_frozen_state () =
-  add_anonymous_entry (FrozenState (freeze_summaries()))
+  let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
 
 let contents_after = function
   | None -> !lib_stk
   | Some sp -> let (after,_,_) = split_lib sp in after
 
+let map_leaf sp = 
+  match Hashtbl.find lib_tab sp with
+    | Leaf obj -> obj
+    | _ -> anomaly "Lib.map_leaf: not a leaf"
 
 (* Sections. *)