module Library

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

1 files changed, 6 insertions, 2 deletions

diff --git a/library/lib.ml b/library/lib.ml
index a8ab156c57..42850bc052 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -20,7 +20,11 @@ type library_entry = section_path * node
 
 
 (* We keep trace of operations in a stack [lib_stk]. 
-   [path_prefix] is the current path of sections (in correct order). *)
+   [path_prefix] is the current path of sections. Sections are stored in 
+   ``correct'' order, the oldest coming first in the list. It may seems 
+   costly, but in practice there is not so many openings and closings of
+   sections, but on the contrary there are many constructions of section
+   paths. *) 
 
 let lib_stk = ref ([] : (section_path * node) list)
 
@@ -122,7 +126,7 @@ let close_section s =
   in
   let (after,_,before) = split_lib sp in
   lib_stk := before;
-  add_entry sp (ClosedSection (s,modp,after));
+  add_entry sp (ClosedSection (s,modp,List.rev after));
   add_frozen_state ();
   pop_path_prefix ()