diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 8 |
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 |