aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/goptions.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/goptions.mli')
-rw-r--r--library/goptions.mli8
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. *)