From 57570e4dfa9588f51c5148932849a847cb30accb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 25 Oct 2000 15:07:53 +0000
Subject: 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
---
 library/lib.ml | 8 ++++----
 1 file 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
 
-- 
cgit v1.2.3