1 files changed, 1 insertions, 84 deletions
diff --git a/library/nameops.ml b/library/nameops.ml
index ecbe07e77..0fd9ec0d1 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -143,12 +143,7 @@ let next_name_away name l =
     | Name str  -> next_ident_away str l
     | Anonymous -> id_of_string "_"
 
-(**********************************************)
-
-let pr_dirpath sl = (str (string_of_dirpath sl))
-
-(* Operations on dirpaths *)
-let empty_dirpath = make_dirpath []
+let pr_lab l = str (string_of_label l)
 
 let default_module_name = id_of_string "Top"
 let default_module = make_dirpath [default_module_name]
@@ -157,81 +152,3 @@ let default_module = make_dirpath [default_module_name]
 let coq_root = id_of_string "Coq"
 let default_root_prefix = make_dirpath []
 
-let restrict_path n sp =
-  let dir, s = repr_path sp in
-  let (dir',_) = list_chop n (repr_dirpath dir) in
-  Names.make_path (make_dirpath dir') s
-
-(* Pop the last n module idents *)
-let extract_dirpath_prefix n dir =
-  let (_,dir') = list_chop n (repr_dirpath dir) in
-  make_dirpath dir'
-
-let dirpath_prefix p = match repr_dirpath p with
-  | [] -> anomaly "dirpath_prefix: empty dirpath"
-  | _::l -> make_dirpath l
-
-let is_dirpath_prefix_of d1 d2 =
-  list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath 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])
-
-let split_dirpath d =
-  let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
-
-let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
-
-
-(* Section paths *)
-
-let dirpath sp = let (p,_) = repr_path sp in p
-let basename sp = let (_,id) = repr_path sp in id
-
-let path_of_constructor env ((sp,tyi),ind) =
-   let mib = Environ.lookup_mind sp env in
-   let mip = mib.mind_packets.(tyi) in 
-   let (pa,_) = repr_path sp in 
-   Names.make_path pa (mip.mind_consnames.(ind-1))
-
-let path_of_inductive env (sp,tyi) =
-  if tyi = 0 then sp
-  else
-    let mib = Environ.lookup_mind sp env in
-    let mip = mib.mind_packets.(tyi) in 
-    let (pa,_) = repr_path sp in 
-    Names.make_path pa (mip.mind_typename) 
-
-(* parsing *)
-let parse_sp s =
-  let len = String.length s in
-  let rec decoupe_dirs n =
-    try
-      let pos = String.index_from s n '.' in
-      let dir = String.sub s n (pos-n) in
-      let dirs,n' = decoupe_dirs (succ pos) in
-      (id_of_string dir)::dirs,n'
-    with
-      | Not_found -> [],n
-  in
-  if len = 0 then invalid_arg "parse_section_path";
-  let dirs,n = decoupe_dirs 0 in
-  let id = String.sub s n (len-n) in
-  make_dirpath (List.rev dirs), (id_of_string id)
-
-let dirpath_of_string s =
-  try
-    let sl,s = parse_sp s in
-    extend_dirpath sl s
-  with
-    | Invalid_argument _ -> invalid_arg "dirpath_of_string"
-
-let path_of_string s =
-  try
-    let sl,s = parse_sp s in
-    make_path sl s
-  with
-    | Invalid_argument _ -> invalid_arg "path_of_string"
-
-(* Section paths *)
-let pr_sp sp = (str (string_of_path sp))