Bug pop_path_prefix : List.rev manquant

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

1 files changed, 4 insertions, 4 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 41e6ec6e8b..171714c0ec 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -40,12 +40,12 @@ let recalc_path_prefix () =
   path_prefix := recalc !lib_stk
 
 let pop_path_prefix () =
-  let rec pop acc = function
+  let rec pop = function
     | [] -> assert false
-    | [_] -> path_prefix := acc
-    | s::l -> pop (s::acc) l
+    | [_] -> []
+    | s::l -> s :: (pop l)
   in
-  pop [] !path_prefix
+  path_prefix := pop !path_prefix
 
 let make_path id k = Names.make_path !path_prefix id k