Merge PR #7797: Remove reference name type.

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. *)