diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-05 01:18:55 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-05 01:18:55 +0000 |
commit | 95e0512ecb3308ce6d49cfb7af35ba16d123183f (patch) | |
tree | 99ae72183cbae70c3d9b2acba391adab50b47883 /kernel | |
parent | 0c889416f58fa35c9c2afb5c95dc13636101b73d (diff) |
Mini-nettoyage noms longs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1048 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/names.ml | 9 | ||||
-rw-r--r-- | kernel/names.mli | 2 |
2 files changed, 3 insertions, 8 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index a7a2552ff..e785644a5 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 a96534f51..cca174463 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 |