diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-13 00:22:57 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 11:02:58 +0200 |
commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /library/goptions.mli | |
parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (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/goptions.mli')
-rw-r--r-- | library/goptions.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/goptions.mli b/library/goptions.mli index 6c14d19ee..3d7df18fe 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -89,7 +89,7 @@ module MakeRefTable : (A : sig type t val compare : t -> t -> int - val encode : reference -> t + val encode : qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -147,9 +147,9 @@ val get_string_table : val get_ref_table : option_name -> - < add : reference -> unit; - remove : reference -> unit; - mem : reference -> unit; + < add : qualid -> unit; + remove : qualid -> unit; + mem : qualid -> unit; print : unit > (** The first argument is a locality flag. *) |