From 95e0512ecb3308ce6d49cfb7af35ba16d123183f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 5 Dec 2000 01:18:55 +0000
Subject: Mini-nettoyage noms longs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1048 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml  | 9 +++------
 kernel/names.mli | 2 --
 2 files changed, 3 insertions(+), 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index a7a2552ffa..e785644a57 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -163,9 +163,6 @@ let pr_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
 (*s Directory paths = section names paths *)
 type dir_path = string list
 
-(* The root of absolute names *)
-let coq_root = []
-
 (*s Section paths are absolute names *)
 
 type section_path = {
@@ -181,15 +178,15 @@ let basename sp = sp.basename
 let dirpath sp = sp.dirpath
 
 let qualid_of_sp sp =
-  make_qualid (coq_root @ dirpath sp) (string_of_id (basename sp))
+  make_qualid (dirpath sp) (string_of_id (basename sp))
 
 (* parsing and printing of section paths *)
-let string_of_dirpath sl = String.concat "." (coq_root@sl)
+let string_of_dirpath sl = String.concat "." sl
 
 let string_of_path sp =
   let (sl,id,k) = repr_path sp in
   String.concat ""
-    (List.flatten (List.map (fun s -> [s;"."]) (coq_root@sl))
+    (List.flatten (List.map (fun s -> [s;"."]) sl)
      @ [ string_of_id id ])
 
 let parse_sp s =
diff --git a/kernel/names.mli b/kernel/names.mli
index a96534f51e..cca174463c 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -51,8 +51,6 @@ val kind_of_string : string -> path_kind
 (*s Directory paths = section names paths *)
 type dir_path = string list
 
-val coq_root : dir_path
-
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
 
-- 
cgit v1.2.3