diff options
| author | herbelin | 2001-03-01 14:02:59 +0000 |
|---|---|---|
| committer | herbelin | 2001-03-01 14:02:59 +0000 |
| commit | 7b6ed1e95bef26f4ae85d7471985128c0dfdbc15 (patch) | |
| tree | a2beab552c8e57d5db2833494e5cc79e6374cc84 /kernel/names.ml | |
| parent | 2a9a43be51ac61e04ebf3fce902899155b48057f (diff) | |
Déplacement de qualid dans Nametab, hors du noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 83cea889a4..035a5d5059 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -254,16 +254,6 @@ let kind_of_string = function | "obj" -> OBJ | _ -> invalid_arg "kind_of_string" -(*s Section paths *) - -type qualid = string list * identifier - -let make_qualid p s = (p,s) -let repr_qualid q = q - -let string_of_qualid (l,s) = String.concat "." (l@[s]) -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 @@ -281,9 +271,6 @@ let kind_of_path sp = sp.kind let basename sp = sp.basename let dirpath sp = sp.dirpath -let qualid_of_sp sp = - make_qualid (dirpath sp) (string_of_id (basename sp)) - (* parsing and printing of section paths *) let string_of_dirpath sl = String.concat "." sl |