Ajout chop_dirpath

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

1 files changed, 4 insertions, 0 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index b7ec0c223..d4cc60719 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -78,6 +78,10 @@ let dirpath_prefix p = match repr_dirpath p with
 let is_dirpath_prefix_of d1 d2 =
   list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
 
+let chop_dirpath n d =
+  let d1,d2 = list_chop n (List.rev (repr_dirpath d)) in
+  make_dirpath (List.rev d1), make_dirpath (List.rev d2)
+
 (* To know how qualified a name should be to be understood in the current env*)
 let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])