aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-13 00:22:57 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-18 11:02:58 +0200
commit61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch)
treec0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /library/libnames.mli
parentf08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff)
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
Diffstat (limited to 'library/libnames.mli')
-rw-r--r--library/libnames.mli31
1 files changed, 11 insertions, 20 deletions
diff --git a/library/libnames.mli b/library/libnames.mli
index 5f69b1f0f..447eecbb5 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -65,23 +65,28 @@ val restrict_path : int -> full_path -> full_path
qualifications of absolute names, including single identifiers.
The [qualid] are used to access the name table. *)
-type qualid
+type qualid_r
+type qualid = qualid_r CAst.t
-val make_qualid : DirPath.t -> Id.t -> qualid
+val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid
val repr_qualid : qualid -> DirPath.t * Id.t
val qualid_eq : qualid -> qualid -> bool
val pr_qualid : qualid -> Pp.t
val string_of_qualid : qualid -> string
-val qualid_of_string : string -> qualid
+val qualid_of_string : ?loc:Loc.t -> string -> qualid
(** Turns an absolute name, a dirpath, or an Id.t into a
qualified name denoting the same name *)
-val qualid_of_path : full_path -> qualid
-val qualid_of_dirpath : DirPath.t -> qualid
-val qualid_of_ident : Id.t -> qualid
+val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
+val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
+val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+
+val qualid_is_ident : qualid -> bool
+val qualid_path : qualid -> DirPath.t
+val qualid_basename : qualid -> Id.t
(** Both names are passed to objects: a "semantic" [kernel_name], which
can be substituted and a "syntactic" [full_path] which can be printed
@@ -124,20 +129,6 @@ val eq_global_dir_reference :
global_dir_reference -> global_dir_reference -> bool
(** {6 ... } *)
-(** A [reference] is the user-level notion of name. It denotes either a
- global name (referred either by a qualified name or by a single
- name) or a variable *)
-
-type reference_r =
- | Qualid of qualid
- | Ident of Id.t
-type reference = reference_r CAst.t
-
-val eq_reference : reference -> reference -> bool
-val qualid_of_reference : reference -> qualid CAst.t
-val string_of_reference : reference -> string
-val pr_reference : reference -> Pp.t
-val join_reference : reference -> reference -> reference
(** some preset paths *)
val default_library : DirPath.t